1 /-
2 Copyright (c) 2018 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl
5 -/
6 import data.set.finite group_theory.coset data.nat.totient
src └─────────────┘ └────────────────┘ └──────────────┘
7 open function
8
9 variables {α : Type*} {s : set α} {a a₁ a₂ b c: α}
id └─┘
src └─┘
typ └─┘
10
11 -- TODO this lemma isn't used anywhere in this file, and should be moved elsewhere.
12 namespace finset
13 open finset
14
15 lemma mem_range_iff_mem_finset_range_of_mod_eq [decidable_eq α] {f : ℤ → α} {a : α} {n : ℕ}
id └──────────┘ ┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ ┴
16 (hn : 0 < n) (h : ∀i, f (i % n) = f i) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
17 a ∈ set.range f ↔ a ∈ (finset.range n).image (λi, f i) :=
id ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ └───┘ ┴ ┴ ┴
src ┴ └───────┘ ┴ ┴ └──────────┘ └───┘
typ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ └───┘ ┴ ┴ ┴
doc └───────┘ └──────────┘ └───┘
18 suffices (∃i, f (i % n) = a) ↔ ∃i, i < n ∧ f ↑i = a, by simpa [h],
id ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘┴┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st └────────┘
19 have hn' : 0 < (n : ℤ), from int.coe_nat_lt.mpr hn,
id ┴ ┴ ┴ └────────────┘└──┘ └┘
src ┴ ┴ └────────────┘└──┘
typ ┴ ┴ ┴ └────────────┘└──┘ └┘
20 iff.intro
id └───────┘
src └───────┘
typ └───────┘
21 (assume ⟨i, hi⟩,
id ┴┴
typ ┴┴
22 have 0 ≤ i % ↑n, from int.mod_nonneg _ (ne_of_gt hn'),
id ┴ ┴ ┴┴ └────────────┘ └──────┘ └─┘
src ┴ ┴ ┴ └────────────┘ └──────┘
typ ┴ ┴ ┴┴ └────────────┘ └──────┘ └─┘
23 ⟨int.to_nat (i % n),
id └────────┘ ┴ ┴
src └────────┘ ┴
typ └────────┘ ┴ ┴
24 by rw [←int.coe_nat_lt, int.to_nat_of_nonneg this]; exact ⟨int.mod_lt_of_pos i hn', hi⟩⟩)
id └────────────┘ └──────────────────┘ └──┘ └───────────────┘ ┴ └─┘ └┘
src └───┘└────────────┘└┘└──────────────────┘┴ ┴ └────┘ └───────────────┘┴ ┴ └┘ ┴
typ └───┘└────────────┘└┘└──────────────────┘┴└──┘┴ └────┘ └───────────────┘┴┴┴└─┘└┘└┘┴
doc └───┘ └┘ ┴ ┴ └────┘ ┴ ┴ └┘ ┴
txt └───┘ └┘ ┴ ┴ └────┘ ┴ ┴ └┘ ┴
par └───┘ └┘ ┴ ┴ └────┘ ┴ ┴ └┘ ┴
pid └─┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
st └──────────────────┘└─────────────────────────┘┴└───────────────────────────────────┘
25 (assume ⟨i, hi, ha⟩,
id ┴┴
typ ┴┴
26 ⟨i, by rw [int.mod_eq_of_lt (int.coe_zero_le _) (int.coe_nat_lt_coe_nat_of_lt hi), ha]⟩)
id └──────────────┘ └─────────────┘ └──────────────────────────┘ └┘ └┘
src └──┘└──────────────┘┴ └─────────────┘└──┘ └──────────────────────────┘┴ └─┘ ┴
typ └──┘└──────────────┘┴ └─────────────┘└──┘ └──────────────────────────┘┴└┘└─┘└┘┴
doc └──┘ ┴ └──┘ ┴ └─┘ ┴
txt └──┘ ┴ └──┘ ┴ └─┘ ┴
par └──┘ ┴ └──┘ ┴ └─┘ ┴
pid └┘ ┴ └──┘ ┴ └─┘ ┴
st └─────────────────────────────────────────────────────────────────────────┘└──┘┴
27
28 end finset
29
30 lemma conj_inj [group α] {x : α} : function.injective (λ (g : α), x * g * x⁻¹) :=
id └───┘ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└┘
src └───┘ └────────────────┘ ┴ ┴ └┘
typ └───┘ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└┘
31 λ a b h, by simpa [mul_left_inj, mul_right_inj] using h
id ┴ ┴ ┴ └──────────┘ └───────────┘ ┴
src └─────┘└──────────┘└┘└───────────┘└──────┘ └
typ ┴ ┴ ┴ └─────┘└──────────┘└┘└───────────┘└──────┘┴└
doc └─────┘ └┘ └──────┘ └
txt └─────┘ └┘ └──────┘ └
par └─────┘ └┘ └──────┘ └
pid ┴┴ └┘ ┴┴└────┘ └
st └────────────────────────────────────────────
32
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
33 lemma mem_normalizer_fintype [group α] {s : set α} [fintype s] {x : α}
id └───┘ ┴ └─┘ ┴ └─────┘ ┴ ┴
src └───┘ └─┘ └─────┘
typ └───┘ ┴ └─┘ ┴ └─────┘ ┴ ┴
doc └─────┘
34 (h : ∀ n, n ∈ s → x * n * x⁻¹ ∈ s) : x ∈ is_subgroup.normalizer s :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ └────────────────────┘ ┴
src ┴ ┴ ┴ └┘ ┴ ┴ └────────────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ └────────────────────┘ ┴
35 by haveI := classical.prop_decidable;
id └──────────────────────┘
src └───────┘└──────────────────────┘
typ └───────┘└──────────────────────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└─┘
st └───────────────────────────────────
36 haveI := set.fintype_image s (λ n, x * n * x⁻¹); exact
id └───────────────┘ ┴ ┴ ┴└┘
src └───────┘└───────────────┘┴ ┴ └──┘ ┴┴┴ ┴ ┴ └┘┴ └────┘
typ └───────┘└───────────────┘┴┴┴ └──┘ ┴┴┴ ┴ ┴┴└┘┴ └────┘
doc └───────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘
txt └───────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘
par └───────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘
pid ┴└─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────
37 λ n, ⟨h n, λ h₁,
src └──┘ ┴ └┘ └───┘
typ └──┘ ┴ └┘ └───┘
doc └──┘ ┴ └┘ └───┘
txt └──┘ ┴ └┘ └───┘
par └──┘ ┴ └┘ └───┘
pid └──┘ ┴ └┘ └───┘
st ─────────────────
38 have heq : (λ n, x * n * x⁻¹) '' s = s := set.eq_of_subset_of_card_le
id └┘ ┴ └─────────────────────────┘
src └─────┘ └──┘ ┴ ┴ ┴ ┴ └┘└┘┴ ┴┴┴ └──┘└─────────────────────────┘└
typ └─────┘ └──┘ ┴ ┴ ┴ ┴ └┘└┘┴ ┴┴┴ └──┘└─────────────────────────┘└
doc └─────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └
txt └─────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └
par └─────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └
pid └─────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └
st ──────────────────────────────────────────────────────────────────────
39 (λ n ⟨y, hy⟩, hy.2 ▸ h y hy.1) (by rw set.card_image_of_injective s conj_inj),
id ┴ └┘ ┴ └─────────────────────────┘ ┴ └──────┘
src ─┘ └──┘ └┘ └─┘ └─┘ ┴ ┴ ┴ └──┘ ┴└─┘└─────────────────────────┘┴ ┴└──────┘└─┘
typ ─┘ └──┘┴└┘└┘└─┘ └─┘ ┴┴┴ ┴ └──┘ ┴└─┘└─────────────────────────┘┴┴┴└──────┘└─┘
doc ─┘ └──┘ └┘ └─┘ └─┘ ┴ ┴ ┴ └──┘ ┴└─┘ ┴ ┴ └─┘
txt ─┘ └──┘ └┘ └─┘ └─┘ ┴ ┴ ┴ └──┘ ┴└─┘ ┴ ┴ └─┘
par ─┘ └──┘ └┘ └─┘ └─┘ ┴ ┴ ┴ └──┘ ┴└─┘ ┴ ┴ └─┘
pid ─┘ └──┘ └┘ └─┘ └─┘ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └─┘
st ───────────────────────────────────┘└────────────────────────────────────────┘└──
40 have x * n * x⁻¹ ∈ (λ n, x * n * x⁻¹) '' s := heq.symm ▸ h₁,
id ┴ ┴ ┴ └───┘
src └─┘ ┴ ┴ ┴ ┴┴┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ └───┘┴ ┴ └┘
typ └─┘ ┴ ┴ ┴ ┴┴┴ └──┘ ┴ ┴ ┴ ┴┴ └┘ ┴┴└──┘ └───┘┴ ┴ └┘
doc └─┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ └┘
txt └─┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ └┘
par └─┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ └┘
pid └─┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────
41 let ⟨y, hy⟩ := this in conj_inj hy.2 ▸ hy.1⟩
id └┘ ┴
src ┴ └┘ └───┘ └──┘ ┴ └─┘┴┴ └───
typ ┴ └┘└┘└───┘ └──┘ ┴ └─┘┴┴ └───
doc ┴ └┘ └───┘ └──┘ ┴ └─┘ ┴ └───
txt ┴ └┘ └───┘ └──┘ ┴ └─┘ ┴ └───
par ┴ └┘ └───┘ └──┘ ┴ └─┘ ┴ └───
pid ┴ └┘ └───┘ └──┘ ┴ └─┘ ┴ └─┘└
st ─────────────────────────────────────────────
42
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
43 section order_of
44 variables [group α] [fintype α] [decidable_eq α]
id └───┘ └─────┘ └──────────┘
src └───┘ └─────┘ └──────────┘
typ └───┘ └─────┘ └──────────┘
doc └─────┘
45 open quotient_group set
46
47 instance quotient_group.fintype (s : set α) [is_subgroup s] [d : decidable_pred s] :
id └─┘ ┴ └─────────┘ ┴ └────────────┘ ┴
src └─┘ └─────────┘ └────────────┘
typ └─┘ ┴ └─────────┘ ┴ └────────────┘ ┴
doc └─────────┘
48 fintype (quotient s) :=
id └─────┘ └──────┘ ┴
src └─────┘ └──────┘
typ └─────┘ └──────┘ ┴
doc └─────┘ └──────┘
49 @quotient.fintype _ _ (left_rel s) (λ _ _, d _)
id └──────────────┘ └──────┘ ┴ ┴ ┴ ┴
src └──────────────┘ └──────┘
typ └──────────────┘ └──────┘ ┴ ┴ ┴ ┴
50
51 lemma card_eq_card_quotient_mul_card_subgroup (s : set α) [hs : is_subgroup s] [fintype s]
id └─┘ ┴ └─────────┘ ┴ └─────┘ ┴
src └─┘ └─────────┘ └─────┘
typ └─┘ ┴ └─────────┘ ┴ └─────┘ ┴
doc └─────────┘ └─────┘
52 [decidable_pred s] : fintype.card α = fintype.card (quotient s) * fintype.card s :=
id └────────────┘ ┴ └──────────┘ ┴ ┴ └──────────┘ └──────┘ ┴ ┴ └──────────┘ ┴
src └────────────┘ └──────────┘ ┴ └──────────┘ └──────┘ ┴ └──────────┘
typ └────────────┘ ┴ └──────────┘ ┴ ┴ └──────────┘ └──────┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘ └──────┘ └──────────┘
53 by rw ← fintype.card_prod;
id └───────────────┘
src └───┘└───────────────┘
typ └───┘└───────────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st └────────────────────────
54 exact fintype.card_congr (is_subgroup.group_equiv_quotient_times_subgroup hs)
id └────────────────┘ └─────────────────────────────────────────────┘ └┘
src └────┘└────────────────┘┴ └─────────────────────────────────────────────┘┴ └─
typ └────┘└────────────────┘┴ └─────────────────────────────────────────────┘┴└┘└─
doc └────┘ ┴ ┴ └─
txt └────┘ ┴ ┴ └─
par └────┘ ┴ ┴ └─
pid ┴ ┴ ┴ ┴└
st ────────────────────────────────────────────────────────────────────────────────
55
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
56 lemma card_subgroup_dvd_card (s : set α) [is_subgroup s] [fintype s] :
id └─┘ ┴ └─────────┘ ┴ └─────┘ ┴
src └─┘ └─────────┘ └─────┘
typ └─┘ ┴ └─────────┘ ┴ └─────┘ ┴
doc └─────────┘ └─────┘
57 fintype.card s ∣ fintype.card α :=
id └──────────┘ ┴ ┴ └──────────┘ ┴
src └──────────┘ ┴ └──────────┘
typ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘
58 by haveI := classical.prop_decidable; simp [card_eq_card_quotient_mul_card_subgroup s]
id └──────────────────────┘ └─────────────────────────────────────┘ ┴
src └───────┘└──────────────────────┘ └────┘└─────────────────────────────────────┘┴ └─
typ └───────┘└──────────────────────┘ └────┘└─────────────────────────────────────┘┴┴└─
doc └───────┘ └────┘ ┴ └─
txt └───────┘ └────┘ ┴ └─
par └───────┘ └────┘ ┴ └─
pid ┴└─┘ ┴┴ ┴ ┴└
st └────────────────────────────────────────────────────────────────────────────────────
59
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
60 lemma card_quotient_dvd_card (s : set α) [is_subgroup s] [decidable_pred s] [fintype s] :
id └─┘ ┴ └─────────┘ ┴ └────────────┘ ┴ └─────┘ ┴
src └─┘ └─────────┘ └────────────┘ └─────┘
typ └─┘ ┴ └─────────┘ ┴ └────────────┘ ┴ └─────┘ ┴
doc └─────────┘ └─────┘
61 fintype.card (quotient s) ∣ fintype.card α :=
id └──────────┘ └──────┘ ┴ ┴ └──────────┘ ┴
src └──────────┘ └──────┘ ┴ └──────────┘
typ └──────────┘ └──────┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────┘ └──────────┘
62 by simp [card_eq_card_quotient_mul_card_subgroup s]
id └─────────────────────────────────────┘ ┴
src └────┘└─────────────────────────────────────┘┴ └─
typ └────┘└─────────────────────────────────────┘┴┴└─
doc └────┘ ┴ └─
txt └────┘ ┴ └─
par └────┘ ┴ └─
pid ┴┴ ┴ ┴└
st └─────────────────────────────────────────────────
63
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
64 @[simp] lemma card_trivial [fintype (is_subgroup.trivial α)] :
id └─────┘ └─────────────────┘ ┴
src └─────┘ └─────────────────┘
typ └─────┘ └─────────────────┘ ┴
doc └──┘ └─────┘ └─────────────────┘
65 fintype.card (is_subgroup.trivial α) = 1 :=
id └──────────┘ └─────────────────┘ ┴ ┴
src └──────────┘ └─────────────────┘ ┴
typ └──────────┘ └─────────────────┘ ┴ ┴
doc └──────────┘ └─────────────────┘
66 fintype.card_eq_one_iff.2
id └─────────────────────┘┴
src └─────────────────────┘┴
typ └─────────────────────┘┴
67 ⟨⟨(1 : α), by simp⟩, λ ⟨y, hy⟩, subtype.eq $ is_subgroup.mem_trivial.1 hy⟩
id ┴ ┴ └┘ └────────┘ └─────────────────────┘┴
src └──┘ └────────┘ └─────────────────────┘┴
typ ┴ └──┘ ┴ └┘ └────────┘ └─────────────────────┘┴
doc └──┘
txt └──┘
par └──┘
st └───┘
68
69 lemma exists_gpow_eq_one (a : α) : ∃i≠0, a ^ (i:ℤ) = 1 :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
70 have ¬ injective (λi:ℤ, a ^ i),
id ┴ └───────┘ ┴ ┴ ┴ ┴
src ┴ └───────┘ ┴ ┴
typ ┴ └───────┘ ┴ ┴ ┴ ┴
71 from not_injective_infinite_fintype _,
id └────────────────────────────┘
src └────────────────────────────┘
typ └────────────────────────────┘
72 let ⟨i, j, a_eq, ne⟩ := show ∃(i j : ℤ), a ^ i = a ^ j ∧ i ≠ j,
id └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
73 by rw [injective] at this; simpa [classical.not_forall] in
id └───────┘ └──────────────────┘
src └──┘└───────┘└───────┘ └─────┘└──────────────────┘└┘
typ └──┘└───────┘└───────┘ └─────┘└──────────────────┘└┘
doc └──┘ └───────┘ └─────┘ └┘
txt └──┘ └───────┘ └─────┘ └┘
par └──┘ └───────┘ └─────┘ └┘
pid └┘ ┴└──────┘ ┴┴ ┴┴
st └────────────┘┴└─────────────────────────────────────┘
74 have a ^ (i - j) = 1,
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
75 by simp [gpow_add, gpow_neg, a_eq],
id └──────┘ └──────┘ └──┘
src └────┘└──────┘└┘└──────┘└┘ ┴
typ └────┘└──────┘└┘└──────┘└┘└──┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st └──────────────────────────────┘
76 ⟨i - j, sub_ne_zero.mpr ne, this⟩
id ┴ └─────────┘└──┘ └──┘
src ┴ └─────────┘└──┘
typ ┴ └─────────┘└──┘ └──┘
77
78 lemma exists_pow_eq_one (a : α) : ∃i > 0, a ^ i = 1 :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
79 let ⟨i, hi, eq⟩ := exists_gpow_eq_one a in
id └─┘ └────────────────┘ ┴
src └────────────────┘
typ └─┘ └────────────────┘ ┴
80 begin
st └─────
81 cases i,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────┘└─
82 { exact ⟨i, nat.pos_of_ne_zero (by simp [int.of_nat_eq_coe, *] at *), eq⟩ },
id ┴ └────────────────┘ └───────────────┘ └┘
src └────┘ └┘└────────────────┘┴ ┴└────┘└───────────────┘└───────┘└─┘└┘└┘
typ └────┘ ┴└┘└────────────────┘┴ ┴└────┘└───────────────┘└───────┘└─┘└┘└┘
doc └────┘ └┘ ┴ ┴└────┘ └───────┘└─┘ └┘
txt └────┘ └┘ ┴ ┴└────┘ └───────┘└─┘ └┘
par └────┘ └┘ ┴ ┴└────┘ └───────┘└─┘ └┘
pid ┴ └┘ ┴ └─────┘ └──────────┘ ┴┴
st ───┘└──────────────────────────────┘└───────────────────────────────┘└─────┘└┘└
83 { exact ⟨i + 1, dec_trivial, inv_eq_one.1 eq⟩ }
id ┴ ┴ └─────────┘ └────────┘ └┘
src └────┘ ┴┴└──┘└─────────┘└┘└────────┘└─┘└┘└┘
typ └────┘ ┴┴┴└──┘└─────────┘└┘└────────┘└─┘└┘└┘
doc └────┘ ┴ └──┘└─────────┘└┘ └─┘ └┘
txt └────┘ ┴ └──┘ └┘ └─┘ └┘
par └────┘ ┴ └──┘ └┘ └─┘ └┘
pid ┴ ┴ └──┘ └┘ └─┘ ┴┴
st ───────────────────────────────────────────────┘└─
84 end
st ──┘
85
86 /-- `order_of a` is the order of the element `a`, i.e. the `n ≥ 1`, s.t. `a ^ n = 1` -/
87 def order_of (a : α) : ℕ := nat.find (exists_pow_eq_one a)
id ┴ ┴ └──────┘ └───────────────┘ ┴
src ┴ └──────┘ └───────────────┘
typ ┴ ┴ └──────┘ └───────────────┘ ┴
88
89 lemma pow_order_of_eq_one (a : α) : a ^ order_of a = 1 :=
id ┴ ┴ ┴ └──────┘ ┴ ┴
src ┴ └──────┘ ┴
typ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘
90 let ⟨h₁, h₂⟩ := nat.find_spec (exists_pow_eq_one a) in h₂
id └─┘ └┘ └───────────┘ └───────────────┘ ┴
src └───────────┘ └───────────────┘
typ └─┘ └┘ └───────────┘ └───────────────┘ ┴
91
92 lemma order_of_pos (a : α) : order_of a > 0 :=
id ┴ └──────┘ ┴ ┴
src └──────┘ ┴
typ ┴ └──────┘ ┴ ┴
doc └──────┘
93 let ⟨h₁, h₂⟩ := nat.find_spec (exists_pow_eq_one a) in h₁
id └─┘ └┘ └───────────┘ └───────────────┘ ┴
src └───────────┘ └───────────────┘
typ └─┘ └┘ └───────────┘ └───────────────┘ ┴
94
95 private lemma pow_injective_aux {n m : ℕ} (a : α) (h : n ≤ m)
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
96 (hn : n < order_of a) (hm : m < order_of a) (eq : a ^ n = a ^ m) : n = m :=
id ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘
97 decidable.by_contradiction $ assume ne : n ≠ m,
id └────────────────────────┘ ┴ ┴ ┴
src └────────────────────────┘ ┴
typ └────────────────────────┘ ┴ ┴ ┴
98 have h₁ : m - n > 0, from nat.pos_of_ne_zero (by simp [nat.sub_eq_iff_eq_add h, ne.symm]),
id ┴ ┴ ┴ ┴ └────────────────┘ └───────────────────┘ ┴
src ┴ ┴ └────────────────┘ └────┘└───────────────────┘┴ └┘ ┴
typ ┴ ┴ ┴ ┴ └────────────────┘ └────┘└───────────────────┘┴┴└┘└─────┘┴
doc └────┘ ┴ └┘ ┴
txt └────┘ ┴ └┘ ┴
par └────┘ ┴ └┘ ┴
pid ┴┴ ┴ └┘ ┴
st └──────────────────────────────────────┘
99 have h₂ : a ^ (m - n) = 1, by simp [pow_sub _ h, eq],
id ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └┘
src ┴ ┴ ┴ └────┘└─────┘└─┘ └┘└┘┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└─────┘└─┘┴└┘└┘┴
doc └────┘ └─┘ └┘ ┴
txt └────┘ └─┘ └┘ ┴
par └────┘ └─┘ └┘ ┴
pid ┴┴ └─┘ └┘ ┴
st └─────────────────────┘
100 have le : order_of a ≤ m - n, from nat.find_min' (exists_pow_eq_one a) ⟨h₁, h₂⟩,
id └──────┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ └───────────────┘ ┴ └┘ └┘
src └──────┘ ┴ ┴ └───────────┘ └───────────────┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ └───────────────┘ ┴ └┘ └┘
doc └──────┘
101 have lt : m - n < order_of a,
id ┴ ┴ ┴ ┴ └──────┘ ┴
src ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──────┘
102 from (nat.sub_lt_left_iff_lt_add h).mpr $ nat.lt_add_left _ _ _ hm,
id └────────────────────────┘ ┴ └─┘ └─────────────┘ └┘
src └────────────────────────┘ └─┘ └─────────────┘
typ └────────────────────────┘ ┴ └─┘ └─────────────┘ └┘
103 lt_irrefl _ (lt_of_le_of_lt le lt)
id └───────┘ └────────────┘ └┘ └┘
src └───────┘ └────────────┘
typ └───────┘ └────────────┘ └┘ └┘
104
105 lemma pow_injective_of_lt_order_of {n m : ℕ} (a : α)
id ┴ ┴
src ┴
typ ┴ ┴
106 (hn : n < order_of a) (hm : m < order_of a) (eq : a ^ n = a ^ m) : n = m :=
id ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘
107 (le_total n m).elim
id └──────┘ ┴ ┴ └──┘
src └──────┘ └──┘
typ └──────┘ ┴ ┴ └──┘
108 (assume h, pow_injective_aux a h hn hm eq)
id ┴ └───────────────┘ ┴ ┴ └┘ └┘ └┘
src └───────────────┘ └┘
typ ┴ └───────────────┘ ┴ ┴ └┘ └┘ └┘
109 (assume h, (pow_injective_aux a h hm hn eq.symm).symm)
id ┴ └───────────────┘ ┴ ┴ └┘ └┘ └┘└───┘ └──┘
src └───────────────┘ └┘└───┘ └──┘
typ ┴ └───────────────┘ ┴ ┴ └┘ └┘ └┘└───┘ └──┘
110
111 lemma order_of_le_card_univ : order_of a ≤ fintype.card α :=
id └──────┘ ┴ ┴ └──────────┘ ┴
src └──────┘ ┴ └──────────┘
typ └──────┘ ┴ ┴ └──────────┘ ┴
doc └──────┘ └──────────┘
112 finset.card_le_of_inj_on ((^) a)
id └──────────────────────┘ ┴ ┴
src └──────────────────────┘ ┴
typ └──────────────────────┘ ┴ ┴
113 (assume n _, fintype.complete _)
id ┴ ┴ └──────────────┘
src └──────────────┘
typ ┴ ┴ └──────────────┘
114 (assume i j, pow_injective_of_lt_order_of a)
id ┴ ┴ └──────────────────────────┘ ┴
src └──────────────────────────┘
typ ┴ ┴ └──────────────────────────┘ ┴
115
116 lemma pow_eq_mod_order_of {n : ℕ} : a ^ n = a ^ (n % order_of a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──────┘
117 calc a ^ n = a ^ (n % order_of a + order_of a * (n / order_of a)) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src ┴ ┴ ┴ └──────┘ ┴ └──────┘ ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──────┘ └──────┘ └──────┘
118 by rw [nat.mod_add_div]
id └─────────────┘
src └──┘└─────────────┘└─
typ └──┘└─────────────┘└─
doc └──┘ └─
txt └──┘ └─
par └──┘ └─
pid └┘ ┴└
st └──────────────────┘┴└
119 ... = a ^ (n % order_of a) :
id ┴ ┴ ┴ ┴ └──────┘ ┴
src ─┘ ┴ ┴ └──────┘
typ ─┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc ─┘ └──────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
120 by simp [pow_add, pow_mul, pow_order_of_eq_one]
id └─────┘ └─────┘ └─────────────────┘
src └────┘└─────┘└┘└─────┘└┘└─────────────────┘└─
typ └────┘└─────┘└┘└─────┘└┘└─────────────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └─────────────────────────────────────────────
121
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
122 lemma gpow_eq_mod_order_of {i : ℤ} : a ^ i = a ^ (i % order_of a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──────┘
123 calc a ^ i = a ^ (i % order_of a + order_of a * (i / order_of a)) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src ┴ ┴ ┴ └──────┘ ┴ └──────┘ ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──────┘ └──────┘ └──────┘
124 by rw [int.mod_add_div]
id └─────────────┘
src └──┘└─────────────┘└─
typ └──┘└─────────────┘└─
doc └──┘ └─
txt └──┘ └─
par └──┘ └─
pid └┘ ┴└
st └──────────────────┘┴└
125 ... = a ^ (i % order_of a) :
id ┴ ┴ ┴ ┴ └──────┘ ┴
src ─┘ ┴ ┴ └──────┘
typ ─┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc ─┘ └──────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
126 by simp [gpow_add, gpow_mul, pow_order_of_eq_one]
id └──────┘ └──────┘ └─────────────────┘
src └────┘└──────┘└┘└──────┘└┘└─────────────────┘└─
typ └────┘└──────┘└┘└──────┘└┘└─────────────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └───────────────────────────────────────────────
127
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
128 lemma mem_gpowers_iff_mem_range_order_of {a a' : α} :
id ┴
typ ┴
129 a' ∈ gpowers a ↔ a' ∈ (finset.range (order_of a)).image ((^) a : ℕ → α) :=
id └┘ ┴ └─────┘ ┴ ┴ └┘ ┴ └──────────┘ └──────┘ ┴ └───┘ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴ ┴ └──────────┘ └──────┘ └───┘ ┴ ┴
typ └┘ ┴ └─────┘ ┴ ┴ └┘ ┴ └──────────┘ └──────┘ ┴ └───┘ ┴ ┴ ┴ ┴
doc └──────────┘ └──────┘ └───┘
130 finset.mem_range_iff_mem_finset_range_of_mod_eq
id └─────────────────────────────────────────────┘
src └─────────────────────────────────────────────┘
typ └─────────────────────────────────────────────┘
131 (order_of_pos a)
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
132 (assume i, gpow_eq_mod_order_of.symm)
id ┴ └──────────────────┘└───┘
src └──────────────────┘└───┘
typ ┴ └──────────────────┘└───┘
133
134 instance decidable_gpowers : decidable_pred (gpowers a) :=
id └────────────┘ └─────┘ ┴
src └────────────┘ └─────┘
typ └────────────┘ └─────┘ ┴
135 assume a', decidable_of_iff'
id └┘ └───────────────┘
src └───────────────┘
typ └┘ └───────────────┘
136 (a' ∈ (finset.range (order_of a)).image ((^) a))
id └┘ ┴ └──────────┘ └──────┘ ┴ └───┘ ┴ ┴
src ┴ └──────────┘ └──────┘ └───┘ ┴
typ └┘ ┴ └──────────┘ └──────┘ ┴ └───┘ ┴ ┴
doc └──────────┘ └──────┘ └───┘
137 mem_gpowers_iff_mem_range_order_of
id └────────────────────────────────┘
src └────────────────────────────────┘
typ └────────────────────────────────┘
138
139 lemma order_of_dvd_of_pow_eq_one {n : ℕ} (h : a ^ n = 1) : order_of a ∣ n :=
id ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
src ┴ ┴ ┴ └──────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘
140 by_contradiction
id └──────────────┘
src └──────────────┘
typ └──────────────┘
141 (λ h₁, nat.find_min _ (show n % order_of a < order_of a,
id └┘ └──────────┘ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └──────────┘ ┴ └──────┘ ┴ └──────┘
typ └┘ └──────────┘ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴
doc └──────┘ └──────┘
142 from nat.mod_lt _ (order_of_pos _))
id └────────┘ └──────────┘
src └────────┘ └──────────┘
typ └────────┘ └──────────┘
143 ⟨nat.pos_of_ne_zero (mt nat.dvd_of_mod_eq_zero h₁), by rwa ← pow_eq_mod_order_of⟩)
id └────────────────┘ └┘ └────────────────────┘ └┘ └─────────────────┘
src └────────────────┘ └┘ └────────────────────┘ └────┘└─────────────────┘
typ └────────────────┘ └┘ └────────────────────┘ └┘ └────┘└─────────────────┘
doc └────┘
txt └────┘
par └────┘
pid └─┘
st └────────────────────────┘
144
145 lemma order_of_le_of_pow_eq_one {n : ℕ} (hn : 0 < n) (h : a ^ n = 1) : order_of a ≤ n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └──────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘
146 nat.find_min' (exists_pow_eq_one a) ⟨hn, h⟩
id └───────────┘ └───────────────┘ ┴ └┘ ┴
src └───────────┘ └───────────────┘
typ └───────────┘ └───────────────┘ ┴ └┘ ┴
147
148 lemma sum_card_order_of_eq_card_pow_eq_one {n : ℕ} (hn : 0 < n) :
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
149 ((finset.range n.succ).filter (∣ n)).sum (λ m, (finset.univ.filter (λ a : α, order_of a = m)).card)
id └──────────┘ ┴└───┘ └────┘ ┴ ┴ └─┘ ┴ └─────────┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
src └──────────┘ └───┘ └────┘ ┴ └─┘ └─────────┘└─────┘ └──────┘ ┴ └──┘
typ └──────────┘ ┴└───┘ └────┘ ┴ ┴ └─┘ ┴ └─────────┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
doc └──────────┘ └────┘ └─────────┘└─────┘ └──────┘ └──┘
150 = (finset.univ.filter (λ a : α, a ^ n = 1)).card :=
id ┴ └─────────┘└─────┘ ┴ ┴ ┴ ┴ ┴ └──┘
src ┴ └─────────┘└─────┘ ┴ ┴ └──┘
typ ┴ └─────────┘└─────┘ ┴ ┴ ┴ ┴ ┴ └──┘
doc └─────────┘└─────┘ └──┘
151 calc ((finset.range n.succ).filter (∣ n)).sum (λ m, (finset.univ.filter (λ a : α, order_of a = m)).card)
id └──────────┘ ┴└───┘ └────┘ ┴ ┴ └─┘ ┴ └─────────┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
src └──────────┘ └───┘ └────┘ ┴ └─┘ └─────────┘└─────┘ └──────┘ ┴ └──┘
typ └──────────┘ ┴└───┘ └────┘ ┴ ┴ └─┘ ┴ └─────────┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
doc └──────────┘ └────┘ └─────────┘└─────┘ └──────┘ └──┘
152 = _ : (finset.card_bind (by { intros, apply finset.disjoint_filter.2, cc })).symm
id └──────────────┘ └────────────────────┘ └──┘
src └──────────────┘ └────┘ └────┘└────────────────────┘└┘ └─┘ └──┘
typ └──────────────┘ └────┘ └────┘└────────────────────┘└┘ └─┘ └──┘
doc └────┘ └────┘ └┘ └─┘
txt └────┘ └────┘ └┘ └─┘
par └────┘ └────┘ └┘ └─┘
pid ┴ └┘ ┴
st └───────┘└──────────────────────────────┘└───┘└┘
153 ... = _ : congr_arg finset.card (finset.ext.2 (begin
id └───────┘ └─────────┘ └────────┘┴
src └───────┘ └─────────┘ └────────┘┴
typ └───────┘ └─────────┘ └────────┘┴
doc └─────────┘
st └─────
154 assume a,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
155 suffices : order_of a ≤ n ∧ order_of a ∣ n ↔ a ^ n = 1,
id ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴┴┴ ┴ ┴└──────┘┴ ┴┴┴ ┴ ┴ ┴┴┴ ┴┴└┘
typ └─────────┘ ┴ ┴┴┴ ┴ ┴└──────┘┴ ┴┴┴ ┴ ┴┴┴┴┴┴┴┴└┘
doc └─────────┘ ┴ ┴ ┴ ┴ ┴└──────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └───────┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st ───────────────────────────────────────────────────────┘└─
156 { simpa [nat.lt_succ_iff], },
id └─────────────┘
src └─────┘└─────────────┘┴
typ └─────┘└─────────────┘┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ───┘└─────────────────────┘└──┘└
157 exact ⟨λ h, let ⟨m, hm⟩ := h.2 in by rw [hm, pow_mul, pow_order_of_eq_one, _root_.one_pow],
id └┘ └─────┘ └─────────────────┘ └────────────┘
src └────┘ └──┘ ┴ └┘ └───┘ └────┘ ┴└──┘ └┘└─────┘└┘└─────────────────┘└┘└────────────┘┴└─
typ └────┘ └──┘ ┴ └┘ └───┘ └────┘ ┴└──┘└┘└┘└─────┘└┘└─────────────────┘└┘└────────────┘┴└─
doc └────┘ └──┘ ┴ └┘ └───┘ └────┘ ┴└──┘ └┘ └┘ └┘ ┴└─
txt └────┘ └──┘ ┴ └┘ └───┘ └────┘ ┴└──┘ └┘ └┘ └┘ ┴└─
par └────┘ └──┘ ┴ └┘ └───┘ └────┘ ┴└──┘ └┘ └┘ └┘ ┴└─
pid ┴ └──┘ ┴ └┘ └───┘ └────┘ └───┘ └┘ └┘ └┘ └──
st ─────────────────────────────────────┘└─────┘└───────┘└───────────────────┘└──────────────┘┴└─
158 λ h, ⟨order_of_le_of_pow_eq_one hn h, order_of_dvd_of_pow_eq_one h⟩⟩
id └───────────────────────┘ └┘ └────────────────────────┘
src ───┘ └──┘ └───────────────────────┘┴ ┴ └┘└────────────────────────┘┴ └─┘
typ ───┘ └──┘ └───────────────────────┘┴└┘┴ └┘└────────────────────────┘┴ └─┘
doc ───┘ └──┘ ┴ ┴ └┘ ┴ └─┘
txt ───┘ └──┘ ┴ ┴ └┘ ┴ └─┘
par ───┘ └──┘ ┴ ┴ └┘ ┴ └─┘
pid ───┘ └──┘ ┴ ┴ └┘ ┴ └┘┴
st ────────────────────────────────────────────────────────────────────────┘
159 end))
st └─┘
160
161 section
162 local attribute [instance] set_fintype
id └─────────┘
src └─────────┘
typ └─────────┘
163
164 lemma order_eq_card_gpowers : order_of a = fintype.card (gpowers a) :=
id └──────┘ ┴ ┴ └──────────┘ └─────┘ ┴
src └──────┘ ┴ └──────────┘ └─────┘
typ └──────┘ ┴ ┴ └──────────┘ └─────┘ ┴
doc └──────┘ └──────────┘
165 begin
st └─────
166 refine (finset.card_eq_of_bijective _ _ _ _).symm,
id └─────────────────────────┘
src └─────┘ └─────────────────────────┘└────────────┘
typ └─────┘ └─────────────────────────┘└────────────┘
doc └─────┘ └────────────┘
txt └─────┘ └────────────┘
par └─────┘ └────────────┘
pid ┴ └───────────┘┴
st ──────────────────────────────────────────────────┘└─
167 { exact λn hn, ⟨gpow a n, ⟨n, rfl⟩⟩ },
id └──┘ ┴ ┴ └─┘
src └────┘ └────┘ └──┘┴ ┴ └┘┴ └┘└─┘└─┘
typ └────┘ └────┘ └──┘┴┴┴ └┘┴ └┘└─┘└─┘
doc └────┘ └────┘ └──┘┴ ┴ └┘ └┘ └─┘
txt └────┘ └────┘ ┴ ┴ └┘ └┘ └─┘
par └────┘ └────┘ ┴ ┴ └┘ └┘ └─┘
pid ┴ └────┘ ┴ ┴ └┘ └┘ └┘┴
st ───┘└────────────────────────────────┘└┘└
168 { exact assume ⟨_, i, rfl⟩ _,
id ┴
src └────┘ └───┘ └┘ └────
typ └────┘ └───┘┴└┘ └────
doc └────┘ └───┘ └┘ └────
txt └────┘ └───┘ └┘ └────
par └────┘ └───┘ └┘ └────
pid ┴ └───┘ └┘ └────
st ───┘└───────────────────────────
169 have pos: (0:int) < order_of a,
id └─┘ ┴
src ───┘ └────┘ └┘└─┘└┘┴┴ ┴ └─
typ ───┘ └────┘ └┘└─┘└┘┴┴ ┴ └─
doc ───┘ └────┘ └┘ └┘ ┴ ┴ └─
txt ───┘ └────┘ └┘ └┘ ┴ ┴ └─
par ───┘ └────┘ └┘ └┘ ┴ ┴ └─
pid ───┘ └────┘ └┘ └┘ ┴ ┴ └─
st ────────────────────────────────────
170 from int.coe_nat_lt.mpr $ order_of_pos a,
id └────────────────┘ └──────────┘ ┴
src ──────────┘└────────────────┘┴ ┴└──────────┘┴ └─
typ ──────────┘└────────────────┘┴ ┴└──────────┘┴┴└─
doc ──────────┘ ┴ ┴ ┴ └─
txt ──────────┘ ┴ ┴ ┴ └─
par ──────────┘ ┴ ┴ ┴ └─
pid ──────────┘ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────
171 have 0 ≤ i % (order_of a),
id ┴ ┴
src ───┘ └─┘┴┴ ┴┴┴ ┴ └──
typ ───┘ └─┘┴┴ ┴┴┴ ┴ └──
doc ───┘ └─┘ ┴ ┴ ┴ ┴ └──
txt ───┘ └─┘ ┴ ┴ ┴ ┴ └──
par ───┘ └─┘ ┴ ┴ ┴ ┴ └──
pid ───┘ └─┘ ┴ ┴ ┴ ┴ └──
st ───────────────────────────────
172 from int.mod_nonneg _ $ ne_of_gt pos,
id └────────────┘ └──────┘
src ──────────┘└────────────┘└─┘ ┴└──────┘┴ └─
typ ──────────┘└────────────┘└─┘ ┴└──────┘┴ └─
doc ──────────┘ └─┘ ┴ ┴ └─
txt ──────────┘ └─┘ ┴ ┴ └─
par ──────────┘ └─┘ ┴ ┴ └─
pid ──────────┘ └─┘ ┴ ┴ └─
st ────────────────────────────────────────────
173 ⟨int.to_nat (i % order_of a),
id └────────┘ └──────┘
src ───┘ └────────┘┴ ┴ ┴└──────┘┴ └──
typ ───┘ └────────┘┴ ┴ ┴└──────┘┴ └──
doc ───┘ ┴ ┴ ┴└──────┘┴ └──
txt ───┘ ┴ ┴ ┴ ┴ └──
par ───┘ ┴ ┴ ┴ ┴ └──
pid ───┘ ┴ ┴ ┴ ┴ └──
st ──────────────────────────────────
174 by rw [← int.coe_nat_lt, int.to_nat_of_nonneg this];
id └────────────┘ └──────────────────┘ └──┘
src ─────┘ ┴└────┘└────────────┘└┘└──────────────────┘┴ ┴└─
typ ─────┘ ┴└────┘└────────────┘└┘└──────────────────┘┴└──┘┴└─
doc ─────┘ ┴└────┘ └┘ ┴ ┴└─
txt ─────┘ ┴└────┘ └┘ ┴ ┴└─
par ─────┘ ┴└────┘ └┘ ┴ ┴└─
pid ─────┘ └─────┘ └┘ ┴ └──
st ───────┘└───────────────────┘└─────────────────────────┘┴└─
175 exact ⟨int.mod_lt_of_pos _ pos, subtype.eq gpow_eq_mod_order_of.symm⟩⟩ },
id └───────────────┘ └─┘ └────────┘ └───────────────────────┘
src ─────────────┘ └───────────────┘└─┘└─┘└┘└────────┘┴└───────────────────────┘└─┘
typ ─────────────┘ └───────────────┘└─┘└─┘└┘└────────┘┴└───────────────────────┘└─┘
doc ─────────────┘ └─┘ └┘ ┴ └─┘
txt ─────────────┘ └─┘ └┘ ┴ └─┘
par ─────────────┘ └─┘ └┘ ┴ └─┘
pid ─────────────┘ └─┘ └┘ ┴ └┘┴
st ────────────────────────────────────────────────────────────────────────────┘└┘└┘└
176 { intros, exact finset.mem_univ _ },
id └─────────────┘
src └────┘ └────┘└─────────────┘└─┘
typ └────┘ └────┘└─────────────┘└─┘
doc └────┘ └────┘ └─┘
txt └────┘ └────┘ └─┘
par └────┘ └────┘ └─┘
pid ┴ └┘┴
st ───┘└────┘└────────────────────────┘└┘└
177 { exact assume i j hi hj eq, pow_injective_of_lt_order_of a hi hj $ by simpa using eq }
id └──────────────────────────┘ ┴ └┘
src └────┘ └─────────────┘└──────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴└──────────┘└┘┴
typ └────┘ └─────────────┘└──────────────────────────┘┴┴┴ ┴ ┴ ┴ ┴└──────────┘└┘┴
doc └────┘ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──────────┘ ┴
txt └────┘ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──────────┘ ┴
par └────┘ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──────────┘ ┴
pid ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴
st ───────────────────────────────────────────────────────────────────────┘└──────────────┘└─
178 end
st ──┘
179
180 @[simp] lemma order_of_one : order_of (1 : α) = 1 :=
id └──────┘ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴
doc └──┘ └──────┘
181 by rw [order_eq_card_gpowers, fintype.card_eq_one_iff];
id └───────────────────┘ └─────────────────────┘
src └──┘└───────────────────┘└┘└─────────────────────┘┴
typ └──┘└───────────────────┘└┘└─────────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └────────────────────────┘└───────────────────────┘┴└─
182 exact ⟨⟨1, 0, rfl⟩, λ ⟨a, i, ha⟩, by simp [ha.symm]⟩
id └─┘
src └────┘ └────┘└─┘└─┘ └┘ └┘ └┘ └─┘ ┴└────┘ ┴└─
typ └────┘ └────┘└─┘└─┘ └┘ └┘ └┘ └─┘ ┴└────┘└─────┘┴└─
doc └────┘ └────┘ └─┘ └┘ └┘ └┘ └─┘ ┴└────┘ ┴└─
txt └────┘ └────┘ └─┘ └┘ └┘ └┘ └─┘ ┴└────┘ ┴└─
par └────┘ └────┘ └─┘ └┘ └┘ └┘ └─┘ ┴└────┘ ┴└─
pid ┴ └────┘ └─┘ └┘ └┘ └┘ └─┘ └─────┘ └┘└
st ─────────────────────────────────────┘└─────────────┘└─
183
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
184 @[simp] lemma order_of_eq_one_iff : order_of a = 1 ↔ a = 1 :=
id └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──────┘
185 ⟨λ h, by conv { to_lhs, rw [← pow_one a, ← h, pow_order_of_eq_one] }, λ h, by simp [h]⟩
id ┴ └─────┘ ┴ ┴ └─────────────────┘ ┴ ┴
src └─────┘└────┘└┘└────┘└─────┘┴ └──┘ └┘└─────────────────┘└┘┴ └────┘ ┴
typ ┴ └─────┘└────┘└┘└────┘└─────┘┴┴└──┘┴└┘└─────────────────┘└┘┴ ┴ └────┘┴┴
doc └────┘ ┴
txt └─────┘└────┘└┘└────┘ ┴ └──┘ └┘ └┘┴ └────┘ ┴
par └─────┘└────┘└┘└────┘ ┴ └──┘ └┘ └┘┴ └────┘ ┴
pid ┴└──────────────┘ ┴ └──┘ └┘ └─┘ ┴┴ ┴
st └─────┘└─────┘└───────────────┘└───┘└───────────────────┘ ┴└┘ └───────┘
186
187 section classical
188 open_locale classical
189 open quotient_group
190
191 /- TODO: use cardinal theory, introduce `card : set α → ℕ`, or setup decidability for cosets -/
192 lemma order_of_dvd_card_univ : order_of a ∣ fintype.card α :=
id └──────┘ ┴ ┴ └──────────┘ ┴
src └──────┘ ┴ └──────────┘
typ └──────┘ ┴ ┴ └──────────┘ ┴
doc └──────┘ └──────────┘
193 have ft_prod : fintype (quotient (gpowers a) × (gpowers a)),
id └─────┘ └──────┘ └─────┘ ┴ ┴ └─────┘ ┴
src └─────┘ └──────┘ └─────┘ ┴ └─────┘
typ └─────┘ └──────┘ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └──────┘
194 from fintype.of_equiv α (gpowers.is_subgroup a).group_equiv_quotient_times_subgroup,
id └──────────────┘ ┴ └─────────────────┘ ┴ └─────────────────────────────────┘
src └──────────────┘ └─────────────────┘ └─────────────────────────────────┘
typ └──────────────┘ ┴ └─────────────────┘ ┴ └─────────────────────────────────┘
doc └──────────────┘
195 have ft_s : fintype (gpowers a),
id └─────┘ └─────┘ ┴
src └─────┘ └─────┘
typ └─────┘ └─────┘ ┴
doc └─────┘
196 from @fintype.fintype_prod_right _ _ _ ft_prod _,
id └────────────────────────┘ └─────┘
src └────────────────────────┘
typ └────────────────────────┘ └─────┘
197 have ft_cosets : fintype (quotient (gpowers a)),
id └─────┘ └──────┘ └─────┘ ┴
src └─────┘ └──────┘ └─────┘
typ └─────┘ └──────┘ └─────┘ ┴
doc └─────┘ └──────┘
198 from @fintype.fintype_prod_left _ _ _ ft_prod ⟨⟨1, is_submonoid.one_mem (gpowers a)⟩⟩,
id └───────────────────────┘ └─────┘ └──────────────────┘ └─────┘ ┴
src └───────────────────────┘ └──────────────────┘ └─────┘
typ └───────────────────────┘ └─────┘ └──────────────────┘ └─────┘ ┴
199 have ft : fintype (quotient (gpowers a) × (gpowers a)),
id └─────┘ └──────┘ └─────┘ ┴ ┴ └─────┘ ┴
src └─────┘ └──────┘ └─────┘ ┴ └─────┘
typ └─────┘ └──────┘ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └──────┘
200 from @prod.fintype _ _ ft_cosets ft_s,
id └──────────┘ └───────┘ └──┘
src └──────────┘
typ └──────────┘ └───────┘ └──┘
201 have eq₁ : fintype.card α = @fintype.card _ ft_cosets * @fintype.card _ ft_s,
id └──────────┘ ┴ ┴ └──────────┘ └───────┘ ┴ └──────────┘ └──┘
src └──────────┘ ┴ └──────────┘ ┴ └──────────┘
typ └──────────┘ ┴ ┴ └──────────┘ └───────┘ ┴ └──────────┘ └──┘
doc └──────────┘ └──────────┘ └──────────┘
202 from calc fintype.card α = @fintype.card _ ft_prod :
id └──────────┘ ┴ └──────────┘ └─────┘
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ └─────┘
doc └──────────┘ └──────────┘
203 @fintype.card_congr _ _ _ ft_prod (gpowers.is_subgroup a).group_equiv_quotient_times_subgroup
id └────────────────┘ └─────┘ └─────────────────┘ ┴ └─────────────────────────────────┘
src └────────────────┘ └─────────────────┘ └─────────────────────────────────┘
typ └────────────────┘ └─────┘ └─────────────────┘ ┴ └─────────────────────────────────┘
204 ... = @fintype.card _ (@prod.fintype _ _ ft_cosets ft_s) :
id └──────────┘ └──────────┘ └───────┘ └──┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘ └───────┘ └──┘
doc └──────────┘
205 congr_arg (@fintype.card _) $ subsingleton.elim _ _
id └───────┘ └──────────┘ └───────────────┘
src └───────┘ └──────────┘ └───────────────┘
typ └───────┘ └──────────┘ └───────────────┘
doc └──────────┘
206 ... = @fintype.card _ ft_cosets * @fintype.card _ ft_s :
id └──────────┘ └───────┘ ┴ └──────────┘ └──┘
src └──────────┘ ┴ └──────────┘
typ └──────────┘ └───────┘ ┴ └──────────┘ └──┘
doc └──────────┘ └──────────┘
207 @fintype.card_prod _ _ ft_cosets ft_s,
id └───────────────┘ └───────┘ └──┘
src └───────────────┘
typ └───────────────┘ └───────┘ └──┘
208 have eq₂ : order_of a = @fintype.card _ ft_s,
id └──────┘ ┴ ┴ └──────────┘ └──┘
src └──────┘ ┴ └──────────┘
typ └──────┘ ┴ ┴ └──────────┘ └──┘
doc └──────┘ └──────────┘
209 from calc order_of a = _ : order_eq_card_gpowers
id └──────┘ ┴ └───────────────────┘
src └──────┘ └───────────────────┘
typ └──────┘ ┴ └───────────────────┘
doc └──────┘
210 ... = _ : congr_arg (@fintype.card _) $ subsingleton.elim _ _,
id └───────┘ └──────────┘ └───────────────┘
src └───────┘ └──────────┘ └───────────────┘
typ └───────┘ └──────────┘ └───────────────┘
doc └──────────┘
211 dvd.intro (@fintype.card (quotient (gpowers a)) ft_cosets) $
id └───────┘ └──────────┘ └──────┘ └─────┘ ┴ └───────┘
src └───────┘ └──────────┘ └──────┘ └─────┘
typ └───────┘ └──────────┘ └──────┘ └─────┘ ┴ └───────┘
doc └──────────┘ └──────┘
212 by rw [eq₁, eq₂, mul_comm]
id └─┘ └─┘ └──────┘
src └──┘ └┘ └┘└──────┘└─
typ └──┘└─┘└┘└─┘└┘└──────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └──────┘└───┘└────────┘┴└
213
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
214
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
215 end classical
216
217 @[simp] lemma pow_card_eq_one (a : α) : a ^ fintype.card α = 1 :=
id ┴ ┴ ┴ └──────────┘ ┴ ┴
src ┴ └──────────┘ ┴
typ ┴ ┴ ┴ └──────────┘ ┴ ┴
doc └──┘ └──────────┘
218 let ⟨m, hm⟩ := @order_of_dvd_card_univ _ a _ _ _ in
id └─┘ └────────────────────┘ ┴
src └────────────────────┘
typ └─┘ └────────────────────┘ ┴
219 by simp [hm, pow_mul, pow_order_of_eq_one]
id └┘ └─────┘ └─────────────────┘
src └────┘ └┘└─────┘└┘└─────────────────┘└─
typ └────┘└┘└┘└─────┘└┘└─────────────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └────────────────────────────────────────
220
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
221 lemma powers_eq_gpowers (a : α) : powers a = gpowers a :=
id ┴ └────┘ ┴ ┴ └─────┘ ┴
src └────┘ ┴ └─────┘
typ ┴ └────┘ ┴ ┴ └─────┘ ┴
doc └────┘
222 set.ext (λ x, ⟨λ ⟨n, hn⟩, ⟨n, by simp * at *⟩,
id └─────┘ ┴ ┴┴
src └─────┘ └─────────┘
typ └─────┘ ┴ ┴┴ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid ┴┴┴└──┘
st └──────────┘
223 λ ⟨i, hi⟩, ⟨(i % order_of a).nat_abs,
id ┴┴ ┴ └──────┘ ┴ └─────┘
src ┴ └──────┘ └─────┘
typ ┴┴ ┴ └──────┘ ┴ └─────┘
doc └──────┘
224 by rwa [← gpow_coe_nat, int.nat_abs_of_nonneg (int.mod_nonneg _
id └──────────┘ └───────────────────┘ └────────────┘
src └─────┘└──────────┘└┘└───────────────────┘┴ └────────────┘└──
typ └─────┘└──────────┘└┘└───────────────────┘┴ └────────────┘└──
doc └─────┘ └┘ ┴ └──
txt └─────┘ └┘ ┴ └──
par └─────┘ └┘ ┴ └──
pid └──┘ └┘ ┴ └──
st └──────────────────┘└─────────────────────────────────────────
225 (int.coe_nat_ne_zero_iff_pos.2 (order_of_pos _))), ← gpow_eq_mod_order_of]⟩⟩)
id └─────────────────────────┘ └──────────┘ └──────────────────┘
src ─────┘ └─────────────────────────┘└─┘ └──────────┘└───────┘└──────────────────┘┴
typ ─────┘ └─────────────────────────┘└─┘ └──────────┘└───────┘└──────────────────┘┴
doc ─────┘ └─┘ └───────┘ ┴
txt ─────┘ └─┘ └───────┘ ┴
par ─────┘ └─┘ └───────┘ ┴
pid ─────┘ └─┘ └───────┘ ┴
st ──────────────────────────────────────────────────────┘└──────────────────────┘┴
226
227 open nat
228
229 lemma order_of_pow (a : α) (n : ℕ) : order_of (a ^ n) = order_of a / gcd (order_of a) n :=
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └─┘ └──────┘ ┴ ┴
src ┴ └──────┘ ┴ ┴ └──────┘ ┴ └─┘ └──────┘
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └─┘ └──────┘ ┴ ┴
doc └──────┘ └──────┘ └──────┘
230 dvd_antisymm
id └──────────┘
src └──────────┘
typ └──────────┘
231 (order_of_dvd_of_pow_eq_one
id └────────────────────────┘
src └────────────────────────┘
typ └────────────────────────┘
232 (by rw [← pow_mul, ← nat.mul_div_assoc _ (gcd_dvd_left _ _), mul_comm,
id └─────┘ └───────────────┘ └──────────┘ └──────┘
src └────┘└─────┘└──┘└───────────────┘└─┘ └──────────┘└─────┘└──────┘└─
typ └────┘└─────┘└──┘└───────────────┘└─┘ └──────────┘└─────┘└──────┘└─
doc └────┘ └──┘ └─┘ └─────┘ └─
txt └────┘ └──┘ └─┘ └─────┘ └─
par └────┘ └──┘ └─┘ └─────┘ └─
pid └──┘ └──┘ └─┘ └─────┘ └─
st └────────────┘└────────────────────────────────────────┘└────────┘└─
233 nat.mul_div_assoc _ (gcd_dvd_right _ _), pow_mul, pow_order_of_eq_one, _root_.one_pow]))
id └───────────────┘ └───────────┘ └─────┘ └─────────────────┘ └────────────┘
src ─────┘└───────────────┘└─┘ └───────────┘└─────┘└─────┘└┘└─────────────────┘└┘└────────────┘┴
typ ─────┘└───────────────┘└─┘ └───────────┘└─────┘└─────┘└┘└─────────────────┘└┘└────────────┘┴
doc ─────┘ └─┘ └─────┘ └┘ └┘ ┴
txt ─────┘ └─┘ └─────┘ └┘ └┘ ┴
par ─────┘ └─┘ └─────┘ └┘ └┘ ┴
pid ─────┘ └─┘ └─────┘ └┘ └┘ ┴
st ────────────────────────────────────────────┘└───────┘└───────────────────┘└──────────────┘┴
234 (have gcd_pos : 0 < gcd (order_of a) n, from gcd_pos_of_pos_left n (order_of_pos a),
id ┴ └─┘ └──────┘ ┴ ┴ └─────────────────┘ ┴ └──────────┘ ┴
src ┴ └─┘ └──────┘ └─────────────────┘ └──────────┘
typ ┴ └─┘ └──────┘ ┴ ┴ └─────────────────┘ ┴ └──────────┘ ┴
doc └──────┘
235 have hdvd : order_of a ∣ n * order_of (a ^ n),
id └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
src └──────┘ ┴ ┴ └──────┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘ └──────┘
236 from order_of_dvd_of_pow_eq_one (by rw [pow_mul, pow_order_of_eq_one]),
id └────────────────────────┘ └─────┘ └─────────────────┘
src └────────────────────────┘ └──┘└─────┘└┘└─────────────────┘┴
typ └────────────────────────┘ └──┘└─────┘└┘└─────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └──────────┘└───────────────────┘┴
237 coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd gcd_pos)
id └──────────────────────────┘ └─────────────────────┘ └─────┘
src └──────────────────────────┘ └─────────────────────┘
typ └──────────────────────────┘ └─────────────────────┘ └─────┘
238 (dvd_of_mul_dvd_mul_right gcd_pos
id └──────────────────────┘ └─────┘
src └──────────────────────┘
typ └──────────────────────┘ └─────┘
239 (by rwa [nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc,
id └────────────────┘ └──────────┘ └───────┘
src └───┘└────────────────┘┴ └──────────┘└─────┘└───────┘└─
typ └───┘└────────────────┘┴ └──────────┘└─────┘└───────┘└─
doc └───┘ ┴ └─────┘ └─
txt └───┘ ┴ └─────┘ └─
par └───┘ ┴ └─────┘ └─
pid └┘ ┴ └─────┘ └─
st └─────────────────────────────────────────┘└─────────┘└─
240 nat.div_mul_cancel (gcd_dvd_right _ _), mul_comm])))
id └────────────────┘ └───────────┘ └──────┘
src ───────────┘└────────────────┘┴ └───────────┘└─────┘└──────┘┴
typ ───────────┘└────────────────┘┴ └───────────┘└─────┘└──────┘┴
doc ───────────┘ ┴ └─────┘ ┴
txt ───────────┘ ┴ └─────┘ ┴
par ───────────┘ ┴ └─────┘ ┴
pid ───────────┘ ┴ └─────┘ ┴
st ─────────────────────────────────────────────────┘└────────┘┴
241
242 lemma pow_gcd_card_eq_one_iff {n : ℕ} {a : α} :
id ┴ ┴
src ┴
typ ┴ ┴
243 a ^ n = 1 ↔ a ^ (gcd n (fintype.card α)) = 1 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └──────────┘ ┴ ┴
src ┴ ┴ ┴ ┴ └─┘ └──────────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘
244 ⟨λ h, have hn : order_of a ∣ n, from dvd_of_mod_eq_zero $
id ┴ └──────┘ ┴ ┴ ┴ └────────────────┘
src └──────┘ ┴ └────────────────┘
typ ┴ └──────┘ ┴ ┴ ┴ └────────────────┘
doc └──────┘
245 by_contradiction (λ ha, by rw pow_eq_mod_order_of at h;
id └──────────────┘ └┘ └─────────────────┘
src └──────────────┘ └─┘└─────────────────┘└───┘
typ └──────────────┘ └┘ └─┘└─────────────────┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st └─────────────────────────────
246 exact (not_le_of_gt (nat.mod_lt n (order_of_pos a)))
id └──────────┘ └────────┘ ┴ └──────────┘ ┴
src └────┘ └──────────┘┴ └────────┘┴ ┴ └──────────┘┴ └───
typ └────┘ └──────────┘┴ └────────┘┴┴┴ └──────────┘┴┴└───
doc └────┘ ┴ ┴ ┴ ┴ └───
txt └────┘ ┴ ┴ ┴ ┴ └───
par └────┘ ┴ ┴ ┴ ┴ └───
pid ┴ ┴ ┴ ┴ ┴ └───
st ─────────────────────────────────────────────────────────────
247 (order_of_le_of_pow_eq_one (nat.pos_of_ne_zero ha) h)),
id └───────────────────────┘ └────────────────┘ └┘ ┴
src ─────────┘ └───────────────────────┘┴ └────────────────┘┴ └┘ ┴
typ ─────────┘ └───────────────────────┘┴ └────────────────┘┴└┘└┘┴┴
doc ─────────┘ ┴ ┴ └┘ ┴
txt ─────────┘ ┴ ┴ └┘ ┴
par ─────────┘ ┴ ┴ └┘ ┴
pid ─────────┘ ┴ ┴ └┘ ┴
st ──────────────────────────────────────────────────────────────┘
248 let ⟨m, hm⟩ := dvd_gcd hn order_of_dvd_card_univ in
id └─┘ └─────┘ └┘ └────────────────────┘
src └─────┘ └────────────────────┘
typ └─┘ └─────┘ └┘ └────────────────────┘
249 by rw [hm, pow_mul, pow_order_of_eq_one, _root_.one_pow],
id └┘ └─────┘ └─────────────────┘ └────────────┘
src └──┘ └┘└─────┘└┘└─────────────────┘└┘└────────────┘┴
typ └──┘└┘└┘└─────┘└┘└─────────────────┘└┘└────────────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st └─────┘└───────┘└───────────────────┘└──────────────┘┴
250 λ h, let ⟨m, hm⟩ := gcd_dvd_left n (fintype.card α) in
id ┴ └─┘ └──────────┘ ┴ └──────────┘ ┴
src └──────────┘ └──────────┘
typ ┴ └─┘ └──────────┘ ┴ └──────────┘ ┴
doc └──────────┘
251 by rw [hm, pow_mul, h, _root_.one_pow]⟩
id └┘ └─────┘ ┴ └────────────┘
src └──┘ └┘└─────┘└┘ └┘└────────────┘┴
typ └──┘└┘└┘└─────┘└┘┴└┘└────────────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st └─────┘└───────┘└─┘└──────────────┘┴
252
253 end
254
255 end order_of
256
257 section cyclic
258
259 local attribute [instance] set_fintype
id └─────────┘
src └─────────┘
typ └─────────┘
260
261 class is_cyclic (α : Type*) [group α] : Prop :=
id └───┘ └───┘ ┴
src └───┘
typ └───┘ └───┘ ┴
262 (exists_generator : ∃ g : α, ∀ x, x ∈ gpowers g)
id ┴ ┴┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ ┴ ┴ └─────┘
typ ┴ ┴┴ ┴ ┴ ┴ └─────┘ ┴
263
264 def is_cyclic.comm_group [hg : group α] [is_cyclic α] : comm_group α :=
id └───┘ ┴ └───────┘ ┴ └────────┘ ┴
src └───┘ └───────┘ └────────┘
typ └───┘ ┴ └───────┘ ┴ └────────┘ ┴
265 { mul_comm := λ x y, show x * y = y * x,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
266 from let ⟨g, hg⟩ := is_cyclic.exists_generator α in
id └─┘ └┘ └────────────────────────┘ ┴
src └────────────────────────┘
typ └─┘ └┘ └────────────────────────┘ ┴
267 let ⟨n, hn⟩ := hg x in let ⟨m, hm⟩ := hg y in
id └─┘ └┘ ┴ └─┘ └┘ ┴
typ └─┘ └┘ ┴ └─┘ └┘ ┴
268 hm ▸ hn ▸ gpow_mul_comm _ _ _,
id ┴ ┴ └───────────┘
src ┴ ┴ └───────────┘
typ ┴ ┴ └───────────┘
269 ..hg }
id └┘
typ └┘
270
271 lemma is_cyclic_of_order_of_eq_card [group α] [fintype α] [decidable_eq α]
id └───┘ ┴ └─────┘ ┴ └──────────┘ ┴
src └───┘ └─────┘ └──────────┘
typ └───┘ ┴ └─────┘ ┴ └──────────┘ ┴
doc └─────┘
272 (x : α) (hx : order_of x = fintype.card α) : is_cyclic α :=
id ┴ └──────┘ ┴ ┴ └──────────┘ ┴ └───────┘ ┴
src └──────┘ ┴ └──────────┘ └───────┘
typ ┴ └──────┘ ┴ ┴ └──────────┘ ┴ └───────┘ ┴
doc └──────┘ └──────────┘
273 ⟨⟨x, set.eq_univ_iff_forall.1 $ set.eq_of_subset_of_card_le
id ┴ └────────────────────┘┴ └─────────────────────────┘
src └────────────────────┘┴ └─────────────────────────┘
typ ┴ └────────────────────┘┴ └─────────────────────────┘
274 (set.subset_univ _)
id └─────────────┘
src └─────────────┘
typ └─────────────┘
275 (by rw [fintype.card_congr (equiv.set.univ α), ← hx, order_eq_card_gpowers])⟩⟩
id └────────────────┘ └────────────┘ ┴ └┘ └───────────────────┘
src └──┘└────────────────┘┴ └────────────┘┴ └───┘ └┘└───────────────────┘┴
typ └──┘└────────────────┘┴ └────────────┘┴┴└───┘└┘└┘└───────────────────┘┴
doc └──┘ ┴ ┴ └───┘ └┘ ┴
txt └──┘ ┴ ┴ └───┘ └┘ ┴
par └──┘ ┴ ┴ └───┘ └┘ ┴
pid └┘ ┴ ┴ └───┘ └┘ ┴
st └────────────────────────────────────────┘└────┘└─────────────────────┘┴
276
277 lemma order_of_eq_card_of_forall_mem_gpowers [group α] [fintype α] [decidable_eq α]
id └───┘ ┴ └─────┘ ┴ └──────────┘ ┴
src └───┘ └─────┘ └──────────┘
typ └───┘ ┴ └─────┘ ┴ └──────────┘ ┴
doc └─────┘
278 {g : α} (hx : ∀ x, x ∈ gpowers g) : order_of g = fintype.card α :=
id ┴ ┴ ┴ ┴ └─────┘ ┴ └──────┘ ┴ ┴ └──────────┘ ┴
src ┴ └─────┘ └──────┘ ┴ └──────────┘
typ ┴ ┴ ┴ ┴ └─────┘ ┴ └──────┘ ┴ ┴ └──────────┘ ┴
doc └──────┘ └──────────┘
279 by rw [← fintype.card_congr (equiv.set.univ α), order_eq_card_gpowers];
id └────────────────┘ └────────────┘ ┴ └───────────────────┘
src └────┘└────────────────┘┴ └────────────┘┴ └─┘└───────────────────┘┴
typ └────┘└────────────────┘┴ └────────────┘┴┴└─┘└───────────────────┘┴
doc └────┘ ┴ ┴ └─┘ ┴
txt └────┘ ┴ ┴ └─┘ ┴
par └────┘ ┴ ┴ └─┘ ┴
pid └──┘ ┴ ┴ └─┘ ┴
st └──────────────────────────────────────────┘└─────────────────────┘┴└─
280 simp [hx]; congr
id └┘
src └────┘ ┴ └─────
typ └────┘└┘┴ └─────
doc └────┘ ┴
txt └────┘ ┴ └─────
par └────┘ ┴ └─────
pid ┴┴ ┴ └
st ───────────────────
281
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
282 instance [group α] : is_cyclic (is_subgroup.trivial α) :=
id └───┘ ┴ └───────┘ └─────────────────┘ ┴
src └───┘ └───────┘ └─────────────────┘
typ └───┘ ┴ └───────┘ └─────────────────┘ ┴
doc └─────────────────┘
283 ⟨⟨(1 : is_subgroup.trivial α), λ x, ⟨0, subtype.eq $ eq.symm (is_subgroup.mem_trivial.1 x.2)⟩⟩⟩
id └─────────────────┘ ┴ ┴ └────────┘ └─────┘ └─────────────────────┘┴ ┴┴
src └─────────────────┘ └────────┘ └─────┘ └─────────────────────┘┴ ┴
typ └─────────────────┘ ┴ ┴ └────────┘ └─────┘ └─────────────────────┘┴ ┴┴
doc └─────────────────┘
284
285 instance is_subgroup.is_cyclic [group α] [is_cyclic α] (H : set α) [is_subgroup H] : is_cyclic H :=
id └───┘ ┴ └───────┘ ┴ └─┘ ┴ └─────────┘ ┴ └───────┘ ┴
src └───┘ └───────┘ └─┘ └─────────┘ └───────┘
typ └───┘ ┴ └───────┘ ┴ └─┘ ┴ └─────────┘ ┴ └───────┘ ┴
doc └─────────┘
286 by haveI := classical.prop_decidable; exact
id └──────────────────────┘
src └───────┘└──────────────────────┘ └────┘
typ └───────┘└──────────────────────┘ └────┘
doc └───────┘ └────┘
txt └───────┘ └────┘
par └───────┘ └────┘
pid ┴└─┘ ┴
st └─────────────────────────────────────────
287 let ⟨g, hg⟩ := is_cyclic.exists_generator α in
id ┴ └┘ └────────────────────────┘ ┴
src ┴ └┘ └───┘└────────────────────────┘┴ └──┘
typ ┴ ┴└┘└┘└───┘└────────────────────────┘┴┴└──┘
doc ┴ └┘ └───┘ ┴ └──┘
txt ┴ └┘ └───┘ ┴ └──┘
par ┴ └┘ └───┘ ┴ └──┘
pid ┴ └┘ └───┘ ┴ └──┘
st ───────────────────────────────────────────────
288 if hx : ∃ (x : α), x ∈ H ∧ x ≠ (1 : α) then
id └┘ ┴ ┴ ┴ ┴ ┴
src └┘└────┘┴└────┘ ┴┴┴ ┴┴┴ ┴┴┴ ┴┴┴ └──┘ └──────
typ └┘└────┘┴└────┘ ┴┴┴ ┴┴┴ ┴┴┴ ┴┴┴ └──┘ └──────
doc └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──────
txt └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──────
par └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──────
pid └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──────
st ────────────────────────────────────────────
289 let ⟨x, hx₁, hx₂⟩ := hx in
id ┴ └─┘
src ─┘ ┴ └┘ └┘ └───┘ └───
typ ─┘ ┴ ┴└┘ └┘└─┘└───┘ └───
doc ─┘ ┴ └┘ └┘ └───┘ └───
txt ─┘ ┴ └┘ └┘ └───┘ └───
par ─┘ ┴ └┘ └┘ └───┘ └───
pid ─┘ ┴ └┘ └┘ └───┘ └───
st ─────────────────────────────
290 let ⟨k, hk⟩ := hg x in
id ┴ └┘
src ─┘ ┴ └┘ └───┘ ┴ └───
typ ─┘ ┴ ┴└┘└┘└───┘ ┴ └───
doc ─┘ ┴ └┘ └───┘ ┴ └───
txt ─┘ ┴ └┘ └───┘ ┴ └───
par ─┘ ┴ └┘ └───┘ ┴ └───
pid ─┘ ┴ └┘ └───┘ ┴ └───
st ─────────────────────────
291 have hex : ∃ n : ℕ, 0 < n ∧ g ^ n ∈ H,
id ┴ ┴ ┴
src ─┘ └─────┘ └───┘ └─┘┴┴ ┴ ┴ ┴┴┴ ┴ ┴ └─
typ ─┘ └─────┘ └───┘ └─┘┴┴ ┴ ┴┴┴┴┴ ┴ ┴ └─
doc ─┘ └─────┘ └───┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
txt ─┘ └─────┘ └───┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ─┘ └─────┘ └───┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ─┘ └─────┘ └───┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ─────────────────────────────────────────
292 from ⟨k.nat_abs, nat.pos_of_ne_zero
id └──────┘ └────────────────┘
src ────────┘ └──────┘└┘└────────────────┘└
typ ────────┘ └──────┘└┘└────────────────┘└
doc ────────┘ └┘ └
txt ────────┘ └┘ └
par ────────┘ └┘ └
pid ────────┘ └┘ └
st ────────────────────────────────────────
293 (λ h, hx₂ $ by rw [← hk, int.eq_zero_of_nat_abs_eq_zero h, gpow_zero]),
id └┘ └────────────────────────────┘ ┴ └───────┘
src ─────┘ └──┘ ┴ ┴ ┴└────┘ └┘└────────────────────────────┘┴ └┘└───────┘┴└──
typ ─────┘ └──┘ ┴ ┴ ┴└────┘└┘└┘└────────────────────────────┘┴┴└┘└───────┘┴└──
doc ─────┘ └──┘ ┴ ┴ ┴└────┘ └┘ ┴ └┘ ┴└──
txt ─────┘ └──┘ ┴ ┴ ┴└────┘ └┘ ┴ └┘ ┴└──
par ─────┘ └──┘ ┴ ┴ ┴└────┘ └┘ ┴ └┘ ┴└──
pid ─────┘ └──┘ ┴ ┴ └─────┘ └┘ ┴ └┘ └───
st ───────────────────┘└───────┘└────────────────────────────────┘└─────────┘┴└──
294 match k, hk with
src ───────┘ ┴ └┘ └─────
typ ───────┘ ┴ └┘ └─────
doc ───────┘ ┴ └┘ └─────
txt ───────┘ ┴ └┘ └─────
par ───────┘ ┴ └┘ └─────
pid ───────┘ ┴ └┘ └─────
st ─────────────────────────
295 | (k : ℕ), hk := by rw [int.nat_abs_of_nat, ← gpow_coe_nat, hk]; exact hx₁
id └────────────────┘ └──────────┘ └┘ └─┘
src ─────────┘ └─┘ └─┘ └──┘ ┴└──┘└────────────────┘└──┘└──────────┘└┘ ┴└──────┘ └
typ ─────────┘ └─┘ └─┘ └──┘ ┴└──┘└────────────────┘└──┘└──────────┘└┘└┘┴└──────┘└─┘└
doc ─────────┘ └─┘ └─┘ └──┘ ┴└──┘ └──┘ └┘ ┴└──────┘ └
txt ─────────┘ └─┘ └─┘ └──┘ ┴└──┘ └──┘ └┘ ┴└──────┘ └
par ─────────┘ └─┘ └─┘ └──┘ ┴└──┘ └──┘ └┘ ┴└──────┘ └
pid ─────────┘ └─┘ └─┘ └──┘ └───┘ └──┘ └┘ └───────┘ └
st ──────────────────────────┘└─────────────────────┘└──────────────┘└──┘┴└───────────
296 | -[1+ k], hk := by rw [int.nat_abs_of_neg_succ_of_nat,
id └──┘ ┴ └────────────────────────────┘
src ─────────┘└──┘┴ ┴└┘ └──┘ ┴└──┘└────────────────────────────┘└─
typ ─────────┘└──┘┴ ┴└┘ └──┘ ┴└──┘└────────────────────────────┘└─
doc ─────────┘ ┴ └┘ └──┘ ┴└──┘ └─
txt ─────────┘ ┴ └┘ └──┘ ┴└──┘ └─
par ─────────┘ ┴ └┘ └──┘ ┴└──┘ └─
pid ─────────┘ ┴ └┘ └──┘ └───┘ └─
st ───────┘└─────────────────┘└─────────────────────────────────┘└─
297 ← is_subgroup.inv_mem_iff H]; simp * at *
id └─────────────────────┘ ┴
src ───────────┘└─────────────────────┘┴ ┴└┘└───────────
typ ───────────┘└─────────────────────┘┴┴┴└┘└───────────
doc ───────────┘ ┴ ┴└┘└───────────
txt ───────────┘ ┴ ┴└┘└───────────
par ───────────┘ ┴ ┴└┘└───────────
pid ───────────┘ ┴ └──────────────
st ────────────────────────────────────┘┴└─────────────
298 end⟩,
src ───────┘└─────
typ ───────┘└─────
doc ───────┘└─────
txt ───────┘└─────
par ───────┘└─────
pid ──────────────
st ───────┘└─────
299 ⟨⟨⟨g ^ nat.find hex, (nat.find_spec hex).2⟩,
id └───────────┘
src ─┘ ┴ ┴ ┴ └┘ └───────────┘┴ └─────
typ ─┘ ┴ ┴ ┴ └┘ └───────────┘┴ └─────
doc ─┘ ┴ ┴ ┴ └┘ ┴ └─────
txt ─┘ ┴ ┴ ┴ └┘ ┴ └─────
par ─┘ ┴ ┴ ┴ └┘ ┴ └─────
pid ─┘ ┴ ┴ ┴ └┘ ┴ └─────
st ───────────────────────────────────────────────
300 λ ⟨x, hx⟩, let ⟨k, hk⟩ := hg x in
id ┴
src ───┘ └┘ └┘ └─┘ ┴ └┘ └───┘ ┴ └───
typ ───┘ └┘┴└┘ └─┘ ┴ └┘ └───┘ ┴ └───
doc ───┘ └┘ └┘ └─┘ ┴ └┘ └───┘ ┴ └───
txt ───┘ └┘ └┘ └─┘ ┴ └┘ └───┘ ┴ └───
par ───┘ └┘ └┘ └─┘ ┴ └┘ └───┘ ┴ └───
pid ───┘ └┘ └┘ └─┘ ┴ └┘ └───┘ ┴ └───
st ──────────────────────────────────────
301 have hk₁ : g ^ ((nat.find hex : ℤ) * (k / nat.find hex)) ∈ gpowers (g ^ nat.find hex),
id ┴ ┴ └─────┘
src ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └┘┴┴ ┴┴┴ ┴ └─┘ ┴└─────┘┴ ┴ ┴ ┴ └──
typ ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └┘┴┴ ┴┴┴ ┴ └─┘ ┴└─────┘┴ ┴ ┴ ┴ └──
doc ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──
txt ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──
par ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──
pid ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──
st ─────────────────────────────────────────────────────────────────────────────────────────────
302 from ⟨k / nat.find hex, eq.symm $ gpow_mul _ _ _⟩,
id └──────┘ └─────┘ └──────┘
src ────────────┘ ┴ ┴└──────┘┴ └┘└─────┘┴ ┴└──────┘└────────
typ ────────────┘ ┴ ┴└──────┘┴ └┘└─────┘┴ ┴└──────┘└────────
doc ────────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └────────
txt ────────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └────────
par ────────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └────────
pid ────────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └────────
st ───────────────────────────────────────────────────────────
303 have hk₂ : g ^ ((nat.find hex : ℤ) * (k / nat.find hex)) ∈ H,
src ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─
typ ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─
doc ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─
txt ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─
par ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─
pid ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─
st ────────────────────────────────────────────────────────────────────
304 by rw gpow_mul; exact is_subgroup.gpow_mem (nat.find_spec hex).2,
id └──────┘ └──────────────────┘ └───────────┘ └─┘
src ──────────┘└─┘└──────┘└──────┘└──────────────────┘┴ └───────────┘┴ └────
typ ──────────┘└─┘└──────┘└──────┘└──────────────────┘┴ └───────────┘┴└─┘└────
doc ──────────┘└─┘ └──────┘ ┴ ┴ └────
txt ──────────┘└─┘ └──────┘ ┴ ┴ └────
par ──────────┘└─┘ └──────┘ ┴ ┴ └────
pid ─────────────┘ └──────┘ ┴ ┴ └────
st ─────────┘└────────────────────────────────────────────────────────────┘└─
305 have hk₃ : g ^ (k % nat.find hex) ∈ H,
id ┴
src ─────┘ └─────┘ ┴ ┴ ┴┴┴ ┴ └┘ ┴ └─
typ ─────┘ └─────┘ ┴ ┴ ┴┴┴ ┴ └┘ ┴ └─
doc ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─
txt ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─
par ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─
pid ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─
st ─────────────────────────────────────────────
306 from (is_subgroup.mul_mem_cancel_left H hk₂).1 $
id └─────────────────────────────┘
src ────────────┘ └─────────────────────────────┘┴ ┴ └──┘ └
typ ────────────┘ └─────────────────────────────┘┴ ┴ └──┘ └
doc ────────────┘ ┴ ┴ └──┘ └
txt ────────────┘ ┴ ┴ └──┘ └
par ────────────┘ ┴ ┴ └──┘ └
pid ────────────┘ ┴ ┴ └──┘ └
st ─────────────────────────────────────────────────────────
307 by rw [← gpow_add, int.mod_add_div, hk]; exact hx,
id └──────┘ └─────────────┘ └┘ └┘
src ─────────┘ ┴└────┘└──────┘└┘└─────────────┘└┘ ┴└──────┘ └─
typ ─────────┘ ┴└────┘└──────┘└┘└─────────────┘└┘└┘┴└──────┘└┘└─
doc ─────────┘ ┴└────┘ └┘ └┘ ┴└──────┘ └─
txt ─────────┘ ┴└────┘ └┘ └┘ ┴└──────┘ └─
par ─────────┘ ┴└────┘ └┘ └┘ ┴└──────┘ └─
pid ─────────┘ └─────┘ └┘ └┘ └───────┘ └─
st ───────────┘└─────────────┘└───────────────┘└──┘┴└────────┘└─
308 have hk₄ : k % nat.find hex = (k % nat.find hex).nat_abs,
id ┴
src ─────┘ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └──────────
typ ─────┘ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └──────────
doc ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────
txt ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────
par ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────
pid ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────
st ────────────────────────────────────────────────────────────────
309 by rw int.nat_abs_of_nonneg (int.mod_nonneg _
id └───────────────────┘ └────────────┘
src ──────────┘└─┘└───────────────────┘┴ └────────────┘└──
typ ──────────┘└─┘└───────────────────┘┴ └────────────┘└──
doc ──────────┘└─┘ ┴ └──
txt ──────────┘└─┘ ┴ └──
par ──────────┘└─┘ ┴ └──
pid ─────────────┘ ┴ └──
st ─────────┘└───────────────────────────────────────────
310 (int.coe_nat_ne_zero_iff_pos.2 (nat.find_spec hex).1)),
id └─────────────────────────┘ └───────────┘ └─┘
src ─────────┘ └─────────────────────────┘└─┘ └───────────┘┴ └───┘└─
typ ─────────┘ └─────────────────────────┘└─┘ └───────────┘┴└─┘└───┘└─
doc ─────────┘ └─┘ ┴ └───┘└─
txt ─────────┘ └─┘ ┴ └───┘└─
par ─────────┘ └─┘ ┴ └───┘└─
pid ─────────┘ └─┘ ┴ └──────
st ───────────────────────────────────────────────────────────────┘└─
311 have hk₅ : g ^ (k % nat.find hex ).nat_abs ∈ H,
id └─┘
src ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ └─
typ ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴└─┘└─────────┘ ┴ └─
doc ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ └─
txt ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ └─
par ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ └─
pid ─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ └─
st ──────────────────────────────────────────────────────
312 by rwa [← gpow_coe_nat, ← hk₄],
id └──────────┘ └─┘
src ──────────┘└─────┘└──────────┘└──┘ ┴└─
typ ──────────┘└─────┘└──────────┘└──┘└─┘┴└─
doc ──────────┘└─────┘ └──┘ ┴└─
txt ──────────┘└─────┘ └──┘ ┴└─
par ──────────┘└─────┘ └──┘ ┴└─
pid ─────────────────┘ └──┘ └──
st ─────────┘└──────────────────┘└─────┘┴└─
313 have hk₆ : (k % (nat.find hex : ℤ)).nat_abs = 0,
id └─┘
src ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └─────────┘ └───
typ ─────┘ └─────┘ ┴ ┴ ┴└─┘└─┘ └─────────┘ └───
doc ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └─────────┘ └───
txt ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └─────────┘ └───
par ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └─────────┘ └───
pid ─────┘ └─────┘ ┴ ┴ ┴ └─┘ └─────────┘ └───
st ───────────────────────────────────────────────────────
314 from by_contradiction (λ h,
id └──────────────┘
src ────────────┘└──────────────┘┴ └───
typ ────────────┘└──────────────┘┴ └───
doc ────────────┘ ┴ └───
txt ────────────┘ ┴ └───
par ────────────┘ ┴ └───
pid ────────────┘ ┴ └───
st ────────────────────────────────────
315 nat.find_min hex (int.coe_nat_lt.1 $ by rw [← hk₄];
id └──────────┘ └────────────┘ └─┘
src ─────────┘└──────────┘┴ ┴ └────────────┘└─┘ ┴ ┴└────┘ ┴└─
typ ─────────┘└──────────┘┴ ┴ └────────────┘└─┘ ┴ ┴└────┘└─┘┴└─
doc ─────────┘ ┴ ┴ └─┘ ┴ ┴└────┘ ┴└─
txt ─────────┘ ┴ ┴ └─┘ ┴ ┴└────┘ ┴└─
par ─────────┘ ┴ ┴ └─┘ ┴ ┴└────┘ ┴└─
pid ─────────┘ ┴ ┴ └─┘ ┴ └─────┘ └──
st ────────────────────────────────────────────────┘└────────┘┴└─
316 exact int.mod_lt_of_pos _ (int.coe_nat_pos.2 (nat.find_spec hex).1))
id └───────────────┘ └─────────────┘ └───────────┘ └─┘
src ─────────────────┘└───────────────┘└─┘ └─────────────┘└─┘ └───────────┘┴ └─────
typ ─────────────────┘└───────────────┘└─┘ └─────────────┘└─┘ └───────────┘┴└─┘└─────
doc ─────────────────┘ └─┘ └─┘ ┴ └─────
txt ─────────────────┘ └─┘ └─┘ ┴ └─────
par ─────────────────┘ └─┘ └─┘ ┴ └─────
pid ─────────────────┘ └─┘ └─┘ ┴ └─────
st ──────────────────────────────────────────────────────────────────────────────┘└─
317 ⟨nat.pos_of_ne_zero h, hk₅⟩),
src ─────────┘ ┴ └┘ └───
typ ─────────┘ ┴ └┘ └───
doc ─────────┘ ┴ └┘ └───
txt ─────────┘ ┴ └┘ └───
par ─────────┘ ┴ └┘ └───
pid ─────────┘ ┴ └┘ └───
st ────────────────────────────────────────
318 ⟨k / (nat.find hex : ℤ), subtype.coe_ext.2 begin
id └─┘ └─────────────┘
src ─────┘ ┴ ┴ ┴ └─┘ └─┘└─────────────┘└─┘ └
typ ─────┘ ┴ ┴ ┴└─┘└─┘ └─┘└─────────────┘└─┘ └
doc ─────┘ ┴ ┴ ┴ └─┘ └─┘ └─┘ └
txt ─────┘ ┴ ┴ ┴ └─┘ └─┘ └─┘ └
par ─────┘ ┴ ┴ ┴ └─┘ └─┘ └─┘ └
pid ─────┘ ┴ ┴ ┴ └─┘ └─┘ └─┘ └
st ────────────────────────────────────────────────┘└─────
319 suffices : g ^ ((nat.find hex : ℤ) * (k / nat.find hex)) = x,
id ┴ ┴ └──────┘ └─┘ ┴
src ───────┘└─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴└──────┘┴ └─┘ ┴ └─
typ ───────┘└─────────┘┴┴ ┴ ┴ └─┘ └┘ ┴ ┴┴ ┴└──────┘┴└─┘└─┘ ┴┴└─
doc ───────┘└─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─
txt ───────┘└─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─
par ───────┘└─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─
pid ──────────────────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─
st ───────────────────────────────────────────────────────────────────┘└─
320 { simpa [gpow_mul] },
id └──────┘
src ─────────┘└─────┘└──────┘└┘└──
typ ─────────┘└─────┘└──────┘└┘└──
doc ─────────┘└─────┘ └┘└──
txt ─────────┘└─────┘ └┘└──
par ─────────┘└─────┘ └┘└──
pid ────────────────┘ └────
st ────────┘└────────────────┘┴└─
321 rw [int.mul_div_cancel' (int.dvd_of_mod_eq_zero (int.eq_zero_of_nat_abs_eq_zero hk₆)), hk]
id └─────────────────┘ └────────────────────┘ └────────────────────────────┘ └─┘ └┘
src ───────┘└──┘└─────────────────┘┴ └────────────────────┘┴ └────────────────────────────┘┴ └──┘ └─
typ ───────┘└──┘└─────────────────┘┴ └────────────────────┘┴ └────────────────────────────┘┴└─┘└──┘└┘└─
doc ───────┘└──┘ ┴ ┴ ┴ └──┘ └─
txt ───────┘└──┘ ┴ ┴ ┴ └──┘ └─
par ───────┘└──┘ ┴ ┴ ┴ └──┘ └─
pid ───────────┘ ┴ ┴ ┴ └──┘ └─
st ────────────────────────────────────────────────────────────────────────────────────────────┘└──┘┴└
322 end⟩⟩⟩
src ─────┘└──────
typ ─────┘└──────
doc ─────┘└──────
txt ─────┘└──────
par ─────┘└──────
pid ─────────────
st ─────┘└─┘└───
323 else
src ─────
typ ─────
doc ─────
txt ─────
par ─────
pid ─────
st ─────
324 have H = is_subgroup.trivial α,
id └──┘ └─────────────────┘
src ─┘└──┘└─┘ ┴└─────────────────┘┴ └─
typ ─┘└──┘└─┘ ┴└─────────────────┘┴ └─
doc ─┘ └─┘ ┴└─────────────────┘┴ └─
txt ─┘ └─┘ ┴ ┴ └─
par ─┘ └─┘ ┴ ┴ └─
pid ─┘ └─┘ ┴ ┴ └─
st ──────────────────────────────────
325 from set.ext $ λ x, ⟨λ h, by simp at *; tauto,
id └─────┘
src ────────┘└─────┘┴ ┴ └──┘ └──┘ ┴└───────┘└┘└───┘└─
typ ────────┘└─────┘┴ ┴ └──┘ └──┘ ┴└───────┘└┘└───┘└─
doc ────────┘ ┴ ┴ └──┘ └──┘ ┴└───────┘└┘└───┘└─
txt ────────┘ ┴ ┴ └──┘ └──┘ ┴└───────┘└┘└───┘└─
par ────────┘ ┴ ┴ └──┘ └──┘ ┴└───────┘└┘└───┘└─
pid ────────┘ ┴ ┴ └──┘ └──┘ └──────────────────
st ───────────────────────────────┘└───────────────┘└─
326 λ h, by rw [is_subgroup.mem_trivial.1 h]; exact is_submonoid.one_mem _⟩,
id └─────────────────────┘ ┴ └──────────────────┘
src ─────┘ └──┘ ┴└──┘└─────────────────────┘└─┘ ┴└──────┘└──────────────────┘└────
typ ─────┘ └──┘ ┴└──┘└─────────────────────┘└─┘┴┴└──────┘└──────────────────┘└────
doc ─────┘ └──┘ ┴└──┘ └─┘ ┴└──────┘ └────
txt ─────┘ └──┘ ┴└──┘ └─┘ ┴└──────┘ └────
par ─────┘ └──┘ ┴└──┘ └─┘ ┴└──────┘ └────
pid ─────┘ └──┘ └───┘ └─┘ └───────┘ └────
st ────────────┘└──────────────────────────────┘┴└────────────────────────────┘└──
327 by clear _let_match; subst this; apply_instance
id └──┘
src ─┘ ┴└──────────────┘└┘└────┘ └┘└──────────────
typ ─┘ ┴└──────────────┘└──────┘└──┘└┘└──────────────
doc ─┘ ┴└──────────────┘└┘└────┘ └┘└──────────────
txt ─┘ ┴└──────────────┘└┘└────┘ └┘└──────────────
par ─┘ ┴└──────────────┘└──────┘ └┘└──────────────
pid ─┘ └───────────────────────┘ └────────────────
st ───┘└─────────────────────────────────────────────
328
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
329 open finset nat
330
331 lemma is_cyclic.card_pow_eq_one_le [group α] [fintype α] [decidable_eq α] [is_cyclic α] {n : ℕ}
id └───┘ ┴ └─────┘ ┴ └──────────┘ ┴ └───────┘ ┴ ┴
src └───┘ └─────┘ └──────────┘ └───────┘ ┴
typ └───┘ ┴ └─────┘ ┴ └──────────┘ ┴ └───────┘ ┴ ┴
doc └─────┘
332 (hn0 : 0 < n) : (univ.filter (λ a : α, a ^ n = 1)).card ≤ n :=
id ┴ ┴ └──┘└─────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src ┴ └──┘└─────┘ ┴ ┴ └──┘ ┴
typ ┴ ┴ └──┘└─────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘└─────┘ └──┘
333 let ⟨g, hg⟩ := is_cyclic.exists_generator α in
id └─┘ ┴ └┘ └────────────────────────┘ ┴
src └────────────────────────┘
typ └─┘ ┴ └┘ └────────────────────────┘ ┴
334 calc (univ.filter (λ a : α, a ^ n = 1)).card ≤ (gpowers (g ^ (fintype.card α / (gcd n (fintype.card α))))).to_finset.card :
id └──┘└─────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴ └──────────┘ ┴ ┴ └─┘ ┴ └──────────┘ ┴ └───────┘ └──┘
src └──┘└─────┘ ┴ ┴ └──┘ └─────┘ ┴ └──────────┘ ┴ └─┘ └──────────┘ └───────┘ └──┘
typ └──┘└─────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴ └──────────┘ ┴ ┴ └─┘ ┴ └──────────┘ ┴ └───────┘ └──┘
doc └──┘└─────┘ └──┘ └──────────┘ └──────────┘ └───────┘ └──┘
335 card_le_of_subset (λ x hx, let ⟨m, hm⟩ := show x ∈ powers g, from (powers_eq_gpowers g).symm ▸ hg x in
id └───────────────┘ ┴ └┘ └─┘ ┴ ┴ ┴ └────┘ └───────────────┘ └──┘ ┴ ┴
src └───────────────┘ ┴ └────┘ └───────────────┘ └──┘ ┴
typ └───────────────┘ ┴ └┘ └─┘ ┴ ┴ ┴ └────┘ └───────────────┘ └──┘ ┴ ┴
doc └────┘
336 set.mem_to_finset.2 ⟨(m / (fintype.card α / (gcd n (fintype.card α))) : ℕ),
id └───────────────┘┴ ┴ └──────────┘ ┴ ┴ └─┘ ┴ └──────────┘ ┴ ┴
src └───────────────┘┴ ┴ └──────────┘ ┴ └─┘ └──────────┘ ┴
typ └───────────────┘┴ ┴ └──────────┘ ┴ ┴ └─┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
337 have hgmn : g ^ (m * gcd n (fintype.card α)) = 1,
id ┴ ┴ └─┘ ┴ └──────────┘ ┴ ┴
src ┴ ┴ └─┘ └──────────┘ ┴
typ ┴ ┴ └─┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘
338 by rw [pow_mul, hm, ← pow_gcd_card_eq_one_iff]; exact (mem_filter.1 hx).2,
id └─────┘ └┘ └─────────────────────┘ └────────┘ └┘
src └──┘└─────┘└┘ └──┘└─────────────────────┘┴ └────┘ └────────┘└─┘ └─┘
typ └──┘└─────┘└┘└┘└──┘└─────────────────────┘┴ └────┘ └────────┘└─┘└┘└─┘
doc └──┘ └┘ └──┘ ┴ └────┘ └─┘ └─┘
txt └──┘ └┘ └──┘ ┴ └────┘ └─┘ └─┘
par └──┘ └┘ └──┘ ┴ └────┘ └─┘ └─┘
pid └┘ └┘ └──┘ ┴ ┴ └─┘ ┴└┘
st └──────────┘└──┘└─────────────────────────┘┴└─────────────────────────┘
339 begin
st └─────
340 rw [gpow_coe_nat, ← pow_mul, nat.mul_div_cancel_left', hm],
id └──────────┘ └─────┘ └──────────────────────┘ └┘
src └──┘└──────────┘└──┘└─────┘└┘└──────────────────────┘└┘ ┴
typ └──┘└──────────┘└──┘└─────┘└┘└──────────────────────┘└┘└┘┴
doc └──┘ └──┘ └┘ └┘ ┴
txt └──┘ └──┘ └┘ └┘ ┴
par └──┘ └──┘ └┘ └┘ ┴
pid └┘ └──┘ └┘ └┘ ┴
st ───────────────────────┘└─────────┘└────────────────────────┘└──┘└──
341 refine dvd_of_mul_dvd_mul_right (gcd_pos_of_pos_left (fintype.card α) hn0) _,
id └──────────────────────┘ └─────────────────┘ └──────────┘ ┴ └─┘
src └─────┘└──────────────────────┘┴ └─────────────────┘┴ └──────────┘┴ └┘ └─┘
typ └─────┘└──────────────────────┘┴ └─────────────────┘┴ └──────────┘┴┴└┘└─┘└─┘
doc └─────┘ ┴ ┴ └──────────┘┴ └┘ └─┘
txt └─────┘ ┴ ┴ ┴ └┘ └─┘
par └─────┘ ┴ ┴ ┴ └┘ └─┘
pid ┴ ┴ ┴ ┴ └┘ └─┘
st ───────────────────────────────────────────────────────────────────────────────────┘└─
342 conv {to_lhs, rw [nat.div_mul_cancel (gcd_dvd_right _ _), ← order_of_eq_card_of_forall_mem_gpowers hg]},
id └────────────────┘ └───────────┘ └────────────────────────────────────┘ └┘
src └────┘└────┘└┘└──┘└────────────────┘┴ └───────────┘└───────┘└────────────────────────────────────┘┴ ┴┴
typ └────┘└────┘└┘└──┘└────────────────┘┴ └───────────┘└───────┘└────────────────────────────────────┘┴└┘┴┴
txt └────┘└────┘└┘└──┘ ┴ └───────┘ ┴ ┴┴
par └────┘└────┘└┘└──┘ ┴ └───────┘ ┴ ┴┴
pid ┴└───────────┘ ┴ └───────┘ ┴ └┘
st ─────────────┘└────┘└──────────────────────────────────────────┘└───────────────────────────────────────────┘ └┘└
343 exact order_of_dvd_of_pow_eq_one hgmn
id └────────────────────────┘ └──┘
src └────┘└────────────────────────┘┴ └
typ └────┘└────────────────────────┘┴└──┘└
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴ ┴ └
st ──────────────────────────────────────────────
344 end⟩)
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘└─┘
345 ... ≤ n :
id ┴
typ ┴
346 let ⟨m, hm⟩ := gcd_dvd_right n (fintype.card α) in
id └─┘ ┴ └───────────┘ ┴ └──────────┘ ┴
src └───────────┘ └──────────┘
typ └─┘ ┴ └───────────┘ ┴ └──────────┘ ┴
doc └──────────┘
347 have hm0 : 0 < m, from nat.pos_of_ne_zero
id ┴ └────────────────┘
src ┴ └────────────────┘
typ ┴ └────────────────┘
348 (λ hm0, (by rw [hm0, mul_zero, fintype.card_eq_zero_iff] at hm; exact hm 1)),
id └─┘ └─┘ └──────┘ └──────────────────────┘ └┘
src └──┘ └┘└──────┘└┘└──────────────────────┘└─────┘ └────┘ └┘
typ └─┘ └──┘└─┘└┘└──────┘└┘└──────────────────────┘└─────┘ └────┘└┘└┘
doc └──┘ └┘ └┘ └─────┘ └────┘ └┘
txt └──┘ └┘ └┘ └─────┘ └────┘ └┘
par └──┘ └┘ └┘ └─────┘ └────┘ └┘
pid └┘ └┘ └┘ ┴└────┘ ┴ ┴┴
st └──────┘└────────┘└────────────────────────┘┴└────────────────┘
349 begin
st └─────
350 rw [← fintype.card_of_finset' _ (λ _, set.mem_to_finset), ← order_eq_card_gpowers,
id └─────────────────────┘ └───────────────┘ └───────────────────┘
src └────┘└─────────────────────┘└─┘ └──┘└───────────────┘└───┘└───────────────────┘└─
typ └────┘└─────────────────────┘└─┘ └──┘└───────────────┘└───┘└───────────────────┘└─
doc └────┘ └─┘ └──┘ └───┘ └─
txt └────┘ └─┘ └──┘ └───┘ └─
par └────┘ └─┘ └──┘ └───┘ └─
pid └──┘ └─┘ └──┘ └───┘ └─
st ───────────────────────────────────────────────────────────┘└───────────────────────┘└─
351 order_of_pow, order_of_eq_card_of_forall_mem_gpowers hg],
id └──────────┘ └────────────────────────────────────┘ └┘
src ─────┘└──────────┘└┘└────────────────────────────────────┘┴ ┴
typ ─────┘└──────────┘└┘└────────────────────────────────────┘┴└┘┴
doc ─────┘ └┘ ┴ ┴
txt ─────┘ └┘ ┴ ┴
par ─────┘ └┘ ┴ ┴
pid ─────┘ └┘ ┴ ┴
st ─────────────────┘└─────────────────────────────────────────┘└──
352 rw [hm] {occs := occurrences.pos [2,3]},
id └┘ └─────────────┘ ┴ ┴ ┴
src └──┘ └┘ └──────┘└─────────────┘┴┴┴┴┴┴┴
typ └──┘└┘└┘ └──────┘└─────────────┘┴┴┴┴┴┴┴
doc └──┘ └┘ └──────┘ ┴ ┴ ┴ ┴
txt └──┘ └┘ └──────┘ ┴ ┴ ┴ ┴
par └──┘ └┘ └──────┘ ┴ ┴ ┴ ┴
pid └┘ ┴┴ └──────┘ ┴ ┴ ┴ ┴
st ─────────┘┴└──────────────────────────────┘└─
353 rw [nat.mul_div_cancel_left _ (gcd_pos_of_pos_left _ hn0), gcd_mul_left_left,
id └─────────────────────┘ └─────────────────┘ └─┘ └───────────────┘
src └──┘└─────────────────────┘└──┘ └─────────────────┘└─┘ └─┘└───────────────┘└─
typ └──┘└─────────────────────┘└──┘ └─────────────────┘└─┘└─┘└─┘└───────────────┘└─
doc └──┘ └──┘ └─┘ └─┘ └─
txt └──┘ └──┘ └─┘ └─┘ └─
par └──┘ └──┘ └─┘ └─┘ └─
pid └┘ └──┘ └─┘ └─┘ └─
st ─────────────────────────────────────────────────────────────┘└─────────────────┘└─
354 hm, nat.mul_div_cancel _ hm0],
id └┘ └────────────────┘ └─┘
src ─────┘ └┘└────────────────┘└─┘ ┴
typ ─────┘└┘└┘└────────────────┘└─┘└─┘┴
doc ─────┘ └┘ └─┘ ┴
txt ─────┘ └┘ └─┘ ┴
par ─────┘ └┘ └─┘ ┴
pid ─────┘ └┘ └─┘ ┴
st ───────┘└────────────────────────┘└──
355 exact le_of_dvd hn0 (gcd_dvd_left _ _)
id └───────┘ └─┘ └──────────┘
src └────┘└───────┘┴ ┴ └──────────┘└─────
typ └────┘└───────┘┴└─┘┴ └──────────┘└─────
doc └────┘ ┴ ┴ └─────
txt └────┘ ┴ ┴ └─────
par └────┘ ┴ ┴ └─────
pid ┴ ┴ ┴ └───┘└
st ───────────────────────────────────────────
356 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
357
358 section totient
359
360 variables [group α] [fintype α] [decidable_eq α] (hn : ∀ n : ℕ, 0 < n → (univ.filter (λ a : α, a ^ n = 1)).card ≤ n)
id └───┘ └─────┘ └──────────┘ ┴ ┴ ┴ └──┘└─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └───┘ └─────┘ └──────────┘ ┴ ┴ └──┘└─────┘ ┴ ┴ └──┘ ┴
typ └───┘ └─────┘ └──────────┘ ┴ ┴ ┴ └──┘└─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └─────┘ └──┘└─────┘ └──┘
361 include hn
362
363 lemma card_pow_eq_one_eq_order_of_aux (a : α) :
id ┴
typ ┴
364 (finset.univ.filter (λ b : α, b ^ order_of a = 1)).card = order_of a :=
id └─────────┘└─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └──┘ ┴ └──────┘ ┴
src └─────────┘└─────┘ ┴ └──────┘ ┴ └──┘ ┴ └──────┘
typ └─────────┘└─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └──┘ ┴ └──────┘ ┴
doc └─────────┘└─────┘ └──────┘ └──┘ └──────┘
365 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
366 (hn _ (order_of_pos _))
id └┘ └──────────┘
src └──────────┘
typ └┘ └──────────┘
367 (calc order_of a = @fintype.card (gpowers a) (id _) : order_eq_card_gpowers
id └──────┘ ┴ └──────────┘ └─────┘ ┴ └┘ └───────────────────┘
src └──────┘ └──────────┘ └─────┘ └┘ └───────────────────┘
typ └──────┘ ┴ └──────────┘ └─────┘ ┴ └┘ └───────────────────┘
doc └──────┘ └──────────┘
368 ... ≤ @fintype.card (↑(univ.filter (λ b : α, b ^ order_of a = 1)) : set α)
id └──────────┘ ┴ └──┘└─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─┘ ┴
src └──────────┘ ┴ └──┘└─────┘ ┴ └──────┘ ┴ └─┘
typ └──────────┘ ┴ └──┘└─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─┘ ┴
doc └──────────┘ └──┘└─────┘ └──────┘
369 (fintype.of_finset _ (λ _, iff.rfl)) :
id └───────────────┘ ┴ └─────┘
src └───────────────┘ └─────┘
typ └───────────────┘ ┴ └─────┘
doc └───────────────┘
370 @fintype.card_le_of_injective (gpowers a) (↑(univ.filter (λ b : α, b ^ order_of a = 1)) : set α)
id └──────────────────────────┘ └─────┘ ┴ ┴ └──┘└─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─┘ ┴
src └──────────────────────────┘ └─────┘ ┴ └──┘└─────┘ ┴ └──────┘ ┴ └─┘
typ └──────────────────────────┘ └─────┘ ┴ ┴ └──┘└─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─┘ ┴
doc └──┘└─────┘ └──────┘
371 (id _) (id _) (λ b, ⟨b.1, mem_filter.2 ⟨mem_univ _,
id └┘ └┘ ┴ ┴┴ └────────┘┴ └──────┘
src └┘ └┘ ┴ └────────┘┴ └──────┘
typ └┘ └┘ ┴ ┴┴ └────────┘┴ └──────┘
372 let ⟨i, hi⟩ := b.2 in
id └─┘ ┴┴
src ┴
typ └─┘ ┴┴
373 by rw [← hi, ← gpow_coe_nat, ← gpow_mul, mul_comm, gpow_mul, gpow_coe_nat,
id └┘ └──────────┘ └──────┘ └──────┘ └──────┘ └──────────┘
src └────┘ └──┘└──────────┘└──┘└──────┘└┘└──────┘└┘└──────┘└┘└──────────┘└─
typ └────┘└┘└──┘└──────────┘└──┘└──────┘└┘└──────┘└┘└──────┘└┘└──────────┘└─
doc └────┘ └──┘ └──┘ └┘ └┘ └┘ └─
txt └────┘ └──┘ └──┘ └┘ └┘ └┘ └─
par └────┘ └──┘ └──┘ └┘ └┘ └┘ └─
pid └──┘ └──┘ └──┘ └┘ └┘ └┘ └─
st └───────┘└──────────────┘└──────────┘└────────┘└────────┘└────────────┘└─
374 pow_order_of_eq_one, one_gpow]⟩⟩) (λ _ _ h, subtype.eq (subtype.mk.inj h))
id └─────────────────┘ └──────┘ ┴ ┴ ┴ └────────┘ └────────────┘ ┴
src ───────────┘└─────────────────┘└┘└──────┘┴ └────────┘ └────────────┘
typ ───────────┘└─────────────────┘└┘└──────┘┴ ┴ ┴ ┴ └────────┘ └────────────┘ ┴
doc ───────────┘ └┘ ┴
txt ───────────┘ └┘ ┴
par ───────────┘ └┘ ┴
pid ───────────┘ └┘ ┴
st ──────────────────────────────┘└────────┘┴
375 ... = (univ.filter (λ b : α, b ^ order_of a = 1)).card : fintype.card_of_finset _ _)
id └──┘└─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └──┘ └────────────────────┘
src └──┘└─────┘ ┴ └──────┘ ┴ └──┘ └────────────────────┘
typ └──┘└─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └──┘ └────────────────────┘
doc └──┘└─────┘ └──────┘ └──┘
376
377 open_locale nat -- use φ for nat.totient
378
379 private lemma card_order_of_eq_totient_aux₁ :
380 ∀ {d : ℕ}, d ∣ fintype.card α → 0 < (univ.filter (λ a : α, order_of a = d)).card →
id ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
src ┴ ┴ └──────────┘ ┴ └──┘└─────┘ └──────┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
doc └──────────┘ └──┘└─────┘ └──────┘ └──┘
381 (univ.filter (λ a : α, order_of a = d)).card = φ d
id └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘└─────┘ └──────┘ ┴ └──┘ ┴ ┴
typ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘└─────┘ └──────┘ └──┘
382 | 0 := λ hd hd0,
id └┘ └─┘
typ └┘ └─┘
383 let ⟨a, ha⟩ := card_pos.1 hd0 in absurd (mem_filter.1 ha).2 $ ne_of_gt $ order_of_pos a
id └─┘ ┴ └┘ └──────┘┴ └─┘ └────┘ └────────┘┴ ┴ └──────┘ └──────────┘
src └──────┘┴ └────┘ └────────┘┴ ┴ └──────┘ └──────────┘
typ └─┘ ┴ └┘ └──────┘┴ └─┘ └────┘ └────────┘┴ ┴ └──────┘ └──────────┘
384 | (d+1) := λ hd hd0,
id ┴┴ └┘ └─┘
src ┴
typ ┴┴ └┘ └─┘
385 let ⟨a, ha⟩ := card_pos.1 hd0 in
id └─┘ ┴ └┘ └──────┘┴ └─┘
src └──────┘┴
typ └─┘ ┴ └┘ └──────┘┴ └─┘
386 have ha : order_of a = d.succ, from (mem_filter.1 ha).2,
id └──────┘ ┴ └───┘ └────────┘┴ ┴
src └──────┘ ┴ └───┘ └────────┘┴ ┴
typ └──────┘ ┴ └───┘ └────────┘┴ ┴
doc └──────┘
387 have h : ((range d.succ).filter (∣ d.succ)).sum
id └───┘ └───┘ └────┘ ┴ └───┘ └─┘
src └───┘ └───┘ └────┘ ┴ └───┘ └─┘
typ └───┘ └───┘ └────┘ ┴ └───┘ └─┘
doc └───┘ └────┘
388 (λ m, (univ.filter (λ a : α, order_of a = m)).card) =
id ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴
src └──┘└─────┘ └──────┘ ┴ └──┘ ┴
typ ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴
doc └──┘└─────┘ └──────┘ └──┘
389 ((range d.succ).filter (∣ d.succ)).sum φ, from
id └───┘ └───┘ └────┘ ┴ └───┘ └─┘ ┴
src └───┘ └───┘ └────┘ ┴ └───┘ └─┘ ┴
typ └───┘ └───┘ └────┘ ┴ └───┘ └─┘ ┴
doc └───┘ └────┘
390 finset.sum_congr rfl
id └──────────────┘ └─┘
src └──────────────┘ └─┘
typ └──────────────┘ └─┘
391 (λ m hm, have hmd : m < d.succ, from mem_range.1 (mem_filter.1 hm).1,
id ┴ └┘ ┴ ┴ └───┘ └───────┘┴ └────────┘┴ └┘ ┴
src ┴ └───┘ └───────┘┴ └────────┘┴ ┴
typ ┴ └┘ ┴ ┴ └───┘ └───────┘┴ └────────┘┴ └┘ ┴
392 have hm : m ∣ d.succ, from (mem_filter.1 hm).2,
id ┴ ┴ └───┘ └────────┘┴ └┘ ┴
src ┴ └───┘ └────────┘┴ ┴
typ ┴ ┴ └───┘ └────────┘┴ └┘ ┴
393 card_order_of_eq_totient_aux₁ (dvd.trans hm hd) (finset.card_pos.2
id └───────────────────────────┘ └───────┘ └┘ └┘ └─────────────┘┴
src └───────┘ └─────────────┘┴
typ └───────────────────────────┘ └───────┘ └┘ └┘ └─────────────┘┴
394 ⟨a ^ (d.succ / m), mem_filter.2 ⟨mem_univ _,
id ┴ └───┘ ┴ ┴ └────────┘┴ └──────┘
src ┴ └───┘ ┴ └────────┘┴ └──────┘
typ ┴ └───┘ ┴ ┴ └────────┘┴ └──────┘
395 by rw [order_of_pow, ha, gcd_eq_right (div_dvd_of_dvd hm),
id └──────────┘ └┘ └──────────┘ └────────────┘ └┘
src └──┘└──────────┘└┘ └┘└──────────┘┴ └────────────┘┴ └──
typ └──┘└──────────┘└┘└┘└┘└──────────┘┴ └────────────┘┴└┘└──
doc └──┘ └┘ └┘ ┴ ┴ └──
txt └──┘ └┘ └┘ ┴ ┴ └──
par └──┘ └┘ └┘ ┴ ┴ └──
pid └┘ └┘ └┘ ┴ ┴ └──
st └───────────────┘└──┘└────────────────────────────────┘└─
396 nat.div_div_self hm (succ_pos _)]⟩⟩)),
id └──────────────┘ └┘ └──────┘
src ───────────┘└──────────────┘┴ ┴ └──────┘└──┘
typ ───────────┘└──────────────┘┴└┘┴ └──────┘└──┘
doc ───────────┘ ┴ ┴ └──┘
txt ───────────┘ ┴ ┴ └──┘
par ───────────┘ ┴ ┴ └──┘
pid ───────────┘ ┴ ┴ └──┘
st ───────────────────────────────────────────┘┴
397 have hinsert : insert d.succ ((range d.succ).filter (∣ d.succ))
id └────┘ └───┘ └───┘ └───┘ └────┘ ┴ └───┘
src └────┘ └───┘ └───┘ └───┘ └────┘ ┴ └───┘
typ └────┘ └───┘ └───┘ └───┘ └────┘ ┴ └───┘
doc └───┘ └────┘
398 = (range d.succ.succ).filter (∣ d.succ),
id ┴ └───┘ └────────┘ └────┘ ┴ └───┘
src ┴ └───┘ └────────┘ └────┘ ┴ └───┘
typ ┴ └───┘ └────────┘ └────┘ ┴ └───┘
doc └───┘ └────┘
399 from (finset.ext.2 $ λ x, ⟨λ h, (mem_insert.1 h).elim (λ h, by simp [h, range_succ])
id └────────┘┴ ┴ ┴ └────────┘┴ ┴ └──┘ ┴ ┴ └────────┘
src └────────┘┴ └────────┘┴ └──┘ └────┘ └┘└────────┘┴
typ └────────┘┴ ┴ ┴ └────────┘┴ ┴ └──┘ ┴ └────┘┴└┘└────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └───────────────────┘
400 (by clear _let_match; simp [range_succ]; tauto), by clear _let_match; simp [range_succ] {contextual := tt}; tauto⟩),
id └────────┘ └────────┘ └┘
src └──────────────┘ └────┘└────────┘┴ └───┘ └──────────────┘ └────┘└────────┘└┘ └────────────┘└┘┴ └───┘
typ └──────────────┘ └────┘└────────┘┴ └───┘ └──────────────┘ └────┘└────────┘└┘ └────────────┘└┘┴ └───┘
doc └──────────────┘ └────┘ ┴ └───┘ └──────────────┘ └────┘ └┘ └────────────┘ ┴ └───┘
txt └──────────────┘ └────┘ ┴ └───┘ └──────────────┘ └────┘ └┘ └────────────┘ ┴ └───┘
par └──────────────┘ └────┘ ┴ └───┘ └──────────────┘ └────┘ └┘ └────────────┘ ┴ └───┘
pid └─────────┘ ┴┴ ┴ └─────────┘ ┴┴ ┴┴ └────────────┘ ┴
st └─────────────────────────────────────────┘ └────────────────────────────────────────────────────────────┘
401 have hinsert₁ : d.succ ∉ (range d.succ).filter (∣ d.succ),
id └───┘ ┴ └───┘ └───┘ └────┘ ┴ └───┘
src └───┘ ┴ └───┘ └───┘ └────┘ ┴ └───┘
typ └───┘ ┴ └───┘ └───┘ └────┘ ┴ └───┘
doc └───┘ └────┘
402 by simp [mem_range, zero_le_one, le_succ],
id └───────┘ └─────────┘ └─────┘
src └────┘└───────┘└┘└─────────┘└┘└─────┘┴
typ └────┘└───────┘└┘└─────────┘└┘└─────┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st └─────────────────────────────────────┘
403 (add_right_inj (((range d.succ).filter (∣ d.succ)).sum
id └───────────┘ └───┘ └───┘ └────┘ ┴ └───┘ └─┘
src └───────────┘ └───┘ └───┘ └────┘ ┴ └───┘ └─┘
typ └───────────┘ └───┘ └───┘ └────┘ ┴ └───┘ └─┘
doc └───┘ └────┘
404 (λ m, (univ.filter (λ a : α, order_of a = m)).card))).1
id ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴
src └──┘└─────┘ └──────┘ ┴ └──┘ ┴
typ ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴
doc └──┘└─────┘ └──────┘ └──┘
405 (calc _ = (insert d.succ (filter (∣ d.succ) (range d.succ))).sum
id └────┘ └───┘ └────┘ ┴ └───┘ └───┘ └───┘ └─┘
src └────┘ └───┘ └────┘ ┴ └───┘ └───┘ └───┘ └─┘
typ └────┘ └───┘ └────┘ ┴ └───┘ └───┘ └───┘ └─┘
doc └────┘ └───┘
406 (λ m, (univ.filter (λ a : α, order_of a = m)).card) :
id ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
src └──┘└─────┘ └──────┘ ┴ └──┘
typ ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
doc └──┘└─────┘ └──────┘ └──┘
407 eq.symm (finset.sum_insert (by simp [mem_range, zero_le_one, le_succ]))
id └─────┘ └───────────────┘ └───────┘ └─────────┘ └─────┘
src └─────┘ └───────────────┘ └────┘└───────┘└┘└─────────┘└┘└─────┘┴
typ └─────┘ └───────────────┘ └────┘└───────┘└┘└─────────┘└┘└─────┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st └─────────────────────────────────────┘
408 ... = ((range d.succ.succ).filter (∣ d.succ)).sum (λ m,
id └───┘ └────────┘ └────┘ ┴ └───┘ └─┘ ┴
src └───┘ └────────┘ └────┘ ┴ └───┘ └─┘
typ └───┘ └────────┘ └────┘ ┴ └───┘ └─┘ ┴
doc └───┘ └────┘
409 (univ.filter (λ a : α, order_of a = m)).card) :
id └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
src └──┘└─────┘ └──────┘ ┴ └──┘
typ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
doc └──┘└─────┘ └──────┘ └──┘
410 sum_congr hinsert (λ _ _, rfl)
id └───────┘ └─────┘ ┴ ┴ └─┘
src └───────┘ └─┘
typ └───────┘ └─────┘ ┴ ┴ └─┘
411 ... = (univ.filter (λ a : α, a ^ d.succ = 1)).card :
id └──┘└─────┘ ┴ ┴ ┴ └───┘ ┴ └──┘
src └──┘└─────┘ ┴ └───┘ ┴ └──┘
typ └──┘└─────┘ ┴ ┴ ┴ └───┘ ┴ └──┘
doc └──┘└─────┘ └──┘
412 sum_card_order_of_eq_card_pow_eq_one (succ_pos d)
id └──────────────────────────────────┘ └──────┘
src └──────────────────────────────────┘ └──────┘
typ └──────────────────────────────────┘ └──────┘
413 ... = ((range d.succ.succ).filter (∣ d.succ)).sum φ :
id └───┘ └────────┘ └────┘ ┴ └───┘ └─┘ ┴
src └───┘ └────────┘ └────┘ ┴ └───┘ └─┘ ┴
typ └───┘ └────────┘ └────┘ ┴ └───┘ └─┘ ┴
doc └───┘ └────┘
414 ha ▸ (card_pow_eq_one_eq_order_of_aux hn a).symm ▸ (sum_totient _).symm
id └┘ ┴ └─────────────────────────────┘ └┘ └──┘ ┴ └─────────┘ └──┘
src ┴ └─────────────────────────────┘ └──┘ ┴ └─────────┘ └──┘
typ └┘ ┴ └─────────────────────────────┘ └┘ └──┘ ┴ └─────────┘ └──┘
415 ... = _ : by rw [h, ← sum_insert hinsert₁];
id ┴ └────────┘ └──────┘
src └──┘ └──┘└────────┘┴ ┴
typ └──┘┴└──┘└────────┘┴└──────┘┴
doc └──┘ └──┘ ┴ ┴
txt └──┘ └──┘ ┴ ┴
par └──┘ └──┘ ┴ ┴
pid └┘ └──┘ ┴ ┴
st └────┘└─────────────────────┘┴└─
416 exact finset.sum_congr hinsert.symm (λ _ _, rfl))
id └──────────────┘ └──────────┘ └─┘
src └────┘└──────────────┘┴└──────────┘┴ └────┘└─┘┴
typ └────┘└──────────────┘┴└──────────┘┴ └────┘└─┘┴
doc └────┘ ┴ ┴ └────┘ ┴
txt └────┘ ┴ ┴ └────┘ ┴
par └────┘ ┴ ┴ └────┘ ┴
pid ┴ ┴ ┴ └────┘ ┴
st ─────────────────────────────────────────────────────┘
417
418 lemma card_order_of_eq_totient_aux₂ {d : ℕ} (hd : d ∣ fintype.card α) :
id ┴ ┴ ┴ └──────────┘ ┴
src ┴ ┴ └──────────┘
typ ┴ ┴ ┴ └──────────┘ ┴
doc └──────────┘
419 (univ.filter (λ a : α, order_of a = d)).card = φ d :=
id └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘└─────┘ └──────┘ ┴ └──┘ ┴ ┴
typ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘└─────┘ └──────┘ └──┘
420 by_contradiction $ λ h,
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
421 have h0 : (univ.filter (λ a : α , order_of a = d)).card = 0 :=
id └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴
src └──┘└─────┘ └──────┘ ┴ └──┘ ┴
typ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴
doc └──┘└─────┘ └──────┘ └──┘
422 not_not.1 (mt nat.pos_iff_ne_zero.2 (mt (card_order_of_eq_totient_aux₁ hn hd) h)),
id └─────┘┴ └┘ └─────────────────┘┴ └┘ └───────────────────────────┘ └┘ └┘ ┴
src └─────┘┴ └┘ └─────────────────┘┴ └┘ └───────────────────────────┘
typ └─────┘┴ └┘ └─────────────────┘┴ └┘ └───────────────────────────┘ └┘ └┘ ┴
423 let c := fintype.card α in
id ┴ └──────────┘ ┴
src └──────────┘
typ ┴ └──────────┘ ┴
doc └──────────┘
424 have hc0 : 0 < c, from fintype.card_pos_iff.2 ⟨1⟩,
id ┴ ┴ └──────────────────┘┴
src ┴ └──────────────────┘┴
typ ┴ ┴ └──────────────────┘┴
425 lt_irrefl c $
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
426 calc c = (univ.filter (λ a : α, a ^ c = 1)).card :
id ┴ └──┘└─────┘ ┴ ┴ ┴ ┴ ┴ └──┘
src └──┘└─────┘ ┴ ┴ └──┘
typ ┴ └──┘└─────┘ ┴ ┴ ┴ ┴ ┴ └──┘
doc └──┘└─────┘ └──┘
427 congr_arg card $ by simp [finset.ext, c]
id └───────┘ └──┘ └────────┘ ┴
src └───────┘ └──┘ └────┘└────────┘└┘ └─
typ └───────┘ └──┘ └────┘└────────┘└┘┴└─
doc └──┘ └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └─────────────────────
428 ... = ((range c.succ).filter (∣ c)).sum
id └───┘ ┴└───┘ └────┘ ┴ ┴ └─┘
src ─┘ └───┘ └───┘ └────┘ ┴ └─┘
typ ─┘ └───┘ ┴└───┘ └────┘ ┴ ┴ └─┘
doc ─┘ └───┘ └────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
429 (λ m, (univ.filter (λ a : α, order_of a = m)).card) :
id ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
src └──┘└─────┘ └──────┘ ┴ └──┘
typ ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
doc └──┘└─────┘ └──────┘ └──┘
430 (sum_card_order_of_eq_card_pow_eq_one hc0).symm
id └──────────────────────────────────┘ └─┘ └──┘
src └──────────────────────────────────┘ └──┘
typ └──────────────────────────────────┘ └─┘ └──┘
431 ... = (((range c.succ).filter (∣ c)).erase d).sum
id └───┘ ┴└───┘ └────┘ ┴ ┴ └───┘ ┴ └─┘
src └───┘ └───┘ └────┘ ┴ └───┘ └─┘
typ └───┘ ┴└───┘ └────┘ ┴ ┴ └───┘ ┴ └─┘
doc └───┘ └────┘ └───┘
432 (λ m, (univ.filter (λ a : α, order_of a = m)).card) :
id ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
src └──┘└─────┘ └──────┘ ┴ └──┘
typ ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘
doc └──┘└─────┘ └──────┘ └──┘
433 eq.symm (sum_subset (erase_subset _ _) (λ m hm₁ hm₂,
id └─────┘ └────────┘ └──────────┘ ┴ └─┘ └─┘
src └─────┘ └────────┘ └──────────┘
typ └─────┘ └────────┘ └──────────┘ ┴ └─┘ └─┘
434 have m = d, by simp at *; cc,
id ┴ ┴ ┴
src ┴ └───────┘ └┘
typ ┴ ┴ ┴ └───────┘ └┘
doc └───────┘ └┘
txt └───────┘ └┘
par └───────┘ └┘
pid ┴└──┘
st └────────────┘
435 by simp [*, finset.ext] at *; exact h0))
id └────────┘
src └───────┘└────────┘└────┘ └────┘
typ └───────┘└────────┘└────┘ └────┘
doc └───────┘ └────┘ └────┘
txt └───────┘ └────┘ └────┘
par └───────┘ └────┘ └────┘
pid ┴└──┘ ┴┴└──┘ ┴
st └──────────────────────────────────┘
436 ... ≤ (((range c.succ).filter (∣ c)).erase d).sum φ :
id └───┘ ┴└───┘ └────┘ ┴ ┴ └───┘ ┴ └─┘ ┴
src └───┘ └───┘ └────┘ ┴ └───┘ └─┘ ┴
typ └───┘ ┴└───┘ └────┘ ┴ ┴ └───┘ ┴ └─┘ ┴
doc └───┘ └────┘ └───┘
437 sum_le_sum (λ m hm,
id └────────┘ ┴ └┘
src └────────┘
typ └────────┘ ┴ └┘
438 have hmc : m ∣ c, by simp at hm; tauto,
id ┴ ┴ ┴
src ┴ └────────┘ └───┘
typ ┴ ┴ ┴ └────────┘ └───┘
doc └────────┘ └───┘
txt └────────┘ └───┘
par └────────┘ └───┘
pid ┴└───┘
st └────────────────┘
439 (imp_iff_not_or.1 (card_order_of_eq_totient_aux₁ hn hmc)).elim
id └────────────┘┴ └───────────────────────────┘ └┘ └─┘ └──┘
src └────────────┘┴ └───────────────────────────┘ └──┘
typ └────────────┘┴ └───────────────────────────┘ └┘ └─┘ └──┘
440 (λ h, by simp [nat.le_zero_iff.1 (le_of_not_gt h), nat.zero_le])
id ┴ └─────────────┘ └──────────┘ ┴ └─────────┘
src └────┘└─────────────┘└─┘ └──────────┘┴ └─┘└─────────┘┴
typ ┴ └────┘└─────────────┘└─┘ └──────────┘┴┴└─┘└─────────┘┴
doc └────┘ └─┘ ┴ └─┘ ┴
txt └────┘ └─┘ ┴ └─┘ ┴
par └────┘ └─┘ ┴ └─┘ ┴
pid ┴┴ └─┘ ┴ └─┘ ┴
st └─────────────────────────────────────────────────────┘
441 (by simp [le_refl] {contextual := tt}))
id └─────┘ └┘
src └────┘└─────┘└┘ └────────────┘└┘┴
typ └────┘└─────┘└┘ └────────────┘└┘┴
doc └────┘ └┘ └────────────┘ ┴
txt └────┘ └┘ └────────────┘ ┴
par └────┘ └┘ └────────────┘ ┴
pid ┴┴ ┴┴ └────────────┘ ┴
st └────────────────────────────────┘
442 ... < φ d + (((range c.succ).filter (∣ c)).erase d).sum φ :
id ┴ ┴ ┴ └───┘ ┴└───┘ └────┘ ┴ ┴ └───┘ ┴ └─┘ ┴
src ┴ ┴ └───┘ └───┘ └────┘ ┴ └───┘ └─┘ ┴
typ ┴ ┴ ┴ └───┘ ┴└───┘ └────┘ ┴ ┴ └───┘ ┴ └─┘ ┴
doc └───┘ └────┘ └───┘
443 lt_add_of_pos_left _ (totient_pos (nat.pos_of_ne_zero
id └────────────────┘ └─────────┘ └────────────────┘
src └────────────────┘ └─────────┘ └────────────────┘
typ └────────────────┘ └─────────┘ └────────────────┘
444 (λ h, nat.pos_iff_ne_zero.1 hc0 (eq_zero_of_zero_dvd $ h ▸ hd))))
id ┴ └─────────────────┘┴ └─┘ └─────────────────┘ ┴ ┴ └┘
src └─────────────────┘┴ └─────────────────┘ ┴
typ ┴ └─────────────────┘┴ └─┘ └─────────────────┘ ┴ ┴ └┘
445 ... = (insert d (((range c.succ).filter (∣ c)).erase d)).sum φ : eq.symm (sum_insert (by simp))
id └────┘ ┴ └───┘ ┴└───┘ └────┘ ┴ ┴ └───┘ ┴ └─┘ ┴ └─────┘ └────────┘
src └────┘ └───┘ └───┘ └────┘ ┴ └───┘ └─┘ ┴ └─────┘ └────────┘ └──┘
typ └────┘ ┴ └───┘ ┴└───┘ └────┘ ┴ ┴ └───┘ ┴ └─┘ ┴ └─────┘ └────────┘ └──┘
doc └───┘ └────┘ └───┘ └──┘
txt └──┘
par └──┘
st └───┘
446 ... = ((range c.succ).filter (∣ c)).sum φ : finset.sum_congr
id └───┘ ┴└───┘ └────┘ ┴ ┴ └─┘ ┴ └──────────────┘
src └───┘ └───┘ └────┘ ┴ └─┘ ┴ └──────────────┘
typ └───┘ ┴└───┘ └────┘ ┴ ┴ └─┘ ┴ └──────────────┘
doc └───┘ └────┘
447 (finset.insert_erase (mem_filter.2 ⟨mem_range.2 (lt_succ_of_le (le_of_dvd hc0 hd)), hd⟩)) (λ _ _, rfl)
id └─────────────────┘ └────────┘┴ └───────┘┴ └───────────┘ └───────┘ └─┘ └┘ └┘ ┴ ┴ └─┘
src └─────────────────┘ └────────┘┴ └───────┘┴ └───────────┘ └───────┘ └─┘
typ └─────────────────┘ └────────┘┴ └───────┘┴ └───────────┘ └───────┘ └─┘ └┘ └┘ ┴ ┴ └─┘
448 ... = c : sum_totient _
id ┴ └─────────┘
src └─────────┘
typ ┴ └─────────┘
449
450 lemma is_cyclic_of_card_pow_eq_one_le : is_cyclic α :=
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
451 have (univ.filter (λ a : α, order_of a = fintype.card α)).nonempty,
id └──┘└─────┘ ┴ └──────┘ ┴ ┴ └──────────┘ ┴ └──────┘
src └──┘└─────┘ └──────┘ ┴ └──────────┘ └──────┘
typ └──┘└─────┘ ┴ └──────┘ ┴ ┴ └──────────┘ ┴ └──────┘
doc └──┘└─────┘ └──────┘ └──────────┘ └──────┘
452 from (card_pos.1 $
id └──────┘┴
src └──────┘┴
typ └──────┘┴
453 by rw [card_order_of_eq_totient_aux₂ hn (dvd_refl _)];
id └───────────────────────────┘ └┘ └──────┘
src └──┘└───────────────────────────┘┴ ┴ └──────┘└──┘
typ └──┘└───────────────────────────┘┴└┘┴ └──────┘└──┘
doc └──┘ ┴ ┴ └──┘
txt └──┘ ┴ ┴ └──┘
par └──┘ ┴ ┴ └──┘
pid └┘ ┴ ┴ └──┘
st └────────────────────────────────────────────────┘┴└─
454 exact totient_pos (fintype.card_pos_iff.2 ⟨1⟩)),
id └─────────┘ └──────────────────┘
src └────┘└─────────┘┴ └──────────────────┘└─┘ └─┘
typ └────┘└─────────┘┴ └──────────────────┘└─┘ └─┘
doc └────┘ ┴ └─┘ └─┘
txt └────┘ ┴ └─┘ └─┘
par └────┘ ┴ └─┘ └─┘
pid ┴ ┴ └─┘ └─┘
st ───────────────────────────────────────────────┘
455 let ⟨x, hx⟩ := this in
id └─┘ ┴ └┘ └──┘
typ └─┘ ┴ └┘ └──┘
456 is_cyclic_of_order_of_eq_card x (finset.mem_filter.1 hx).2
id └───────────────────────────┘ └───────────────┘┴ ┴
src └───────────────────────────┘ └───────────────┘┴ ┴
typ └───────────────────────────┘ └───────────────┘┴ ┴
457
458 end totient
459
460 lemma is_cyclic.card_order_of_eq_totient [group α] [is_cyclic α] [fintype α] [decidable_eq α]
id └───┘ ┴ └───────┘ ┴ └─────┘ ┴ └──────────┘ ┴
src └───┘ └───────┘ └─────┘ └──────────┘
typ └───┘ ┴ └───────┘ ┴ └─────┘ ┴ └──────────┘ ┴
doc └─────┘
461 {d : ℕ} (hd : d ∣ fintype.card α) : (univ.filter (λ a : α, order_of a = d)).card = totient d :=
id ┴ ┴ ┴ └──────────┘ ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ └─────┘ ┴
src ┴ ┴ └──────────┘ └──┘└─────┘ └──────┘ ┴ └──┘ ┴ └─────┘
typ ┴ ┴ ┴ └──────────┘ ┴ └──┘└─────┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ └─────┘ ┴
doc └──────────┘ └──┘└─────┘ └──────┘ └──┘
462 card_order_of_eq_totient_aux₂ (λ n, is_cyclic.card_pow_eq_one_le) hd
id └───────────────────────────┘ ┴ └──────────────────────────┘ └┘
src └───────────────────────────┘ └──────────────────────────┘
typ └───────────────────────────┘ ┴ └──────────────────────────┘ └┘
463
464 end cyclic